Mathematical Structures in Computer Science

Công bố khoa học tiêu biểu

* Dữ liệu chỉ mang tính chất tham khảo

Sắp xếp:  
Provable isomorphisms of types
Mathematical 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...... hiện toàn bộ
Introduction to distributive categories
Mathematical 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 this law is satisfied.In any distributive category the coproduct of the final object with itself, 1 + 1, forms a boolean algebra. Thus, maps into 1 + 1 provide a boolean logic: if each such map recognizes a unique subobject, the category is a recognizable distributive category. If, furthermore, the category is such that these recognizers classify detachable subobjects (coproduct embeddings), it is an extensive distributive category.Extensive distributive categories can be approached in various ways. For example, recognizable distributive categories, in which coproducts are disjoint or all preinitials are isomorphic, are extensive. Also, a category X having finite products and binary coproducts satisfying the slice equation hiện toàn bộ
Tripos theory in retrospect
Mathematical Structures in Computer Science - Tập 12 Số 03 - 2002
Andrew M. Pitts
Isomorphic objects in symmetric monoidal closed categories
Mathematical 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 ...... hiện toàn bộ
Reo: a channel-based coordination model for component composition
Mathematical 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 wit...... hiện toàn bộ
A coinductive calculus of streams
Mathematical Structures in Computer Science - Tập 15 Số 1 - Trang 93-147 - 2005
J.J.M.M. Rutten
An experimental library of formalized Mathematics based on the univalent foundations
Mathematical 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 Kapulkin... hiện toàn bộ
Employing UML and OCL for designing and analysing role-based access control
Mathematical Structures in Computer Science - Tập 23 Số 4 - Trang 796-833 - 2013
MIRCO KUHLMANN, KARSTEN SOHR, MARTIN GOGOLLA
Tổng số: 8   
  • 1