Provable isomorphisms of typesMathematical Structures in Computer Science - Tập 2 Số 2 - Trang 231-247 - 1992
Kim B. Bruce, Roberto Di Cosmo, G. Longo
A constructive characterization is given of the isomorphisms which must hold in
all models of the typed lambda calculus with surjective pairing. Using the close
relation between closed Cartesian categories and models of these calculi, we
also produce a characterization of those isomorphisms which hold in all CCC's.
Using the correspondence between these calculi and proofs in intuitionistic
positiv... hiện toàn bộ
Introduction to distributive categoriesMathematical Structures in Computer Science - Tập 3 Số 3 - Trang 277-307 - 1993
J.R.B. Cockett
Distributive category theory is the study of categories with two monoidal
structures, one of which “distributes” over the other in some manner. When these
are the product and coproduct, this distribution is taken to be the lawwhich
asserts that the obvious canonical map has an inverse. A distributive category
is here taken to mean a category with finite products and binary coproducts such
that thi... hiện toàn bộ
Reo: a channel-based coordination model for component compositionMathematical Structures in Computer Science - Tập 14 Số 3 - Trang 329-366 - 2004
Farhad Arbab
In this paper, we present Reo, which forms a paradigm for composition of
software components based on the notion of mobile channels. Reo is a
channel-based exogenous coordination model in which complex coordinators, called
connectors, are compositionally built out of simpler ones. The simplest
connectors in Reo are a set of channels with well-defined behaviour supplied by
users. Reo can be used as... hiện toàn bộ
An experimental library of formalized Mathematics based on the univalent foundationsMathematical Structures in Computer Science - Tập 25 Số 5 - Trang 1278-1294 - 2015
Vladimir Voevodsky
This is a short overview of an experimental library of Mathematics formalized in
the Coq proof assistant using the univalent interpretation of the underlying
type theory of Coq. I started to work on this library in February 2010 in order
to gain experience with formalization of Mathematics in a constructive type
theory based on the intuition gained from the univalent models (see Kapulkinet
al.2012... hiện toàn bộ
Isomorphic objects in symmetric monoidal closed categoriesMathematical Structures in Computer Science - Tập 7 Số 6 - Trang 639-662 - 1997
Kosta Došen, Zoran Petrić
This paper presents a new and self-contained proof of a result characterizing
objects isomorphic in the free symmetric monoidal closed category, i.e., objects
isomorphic in every symmetric monoidal closed category. This characterization is
given by a finitely axiomatizable and decidable equational calculus, which
differs from the calculus that axiomatizes all arithmetical equalities in the
languag... hiện toàn bộ