Types for proofs and programs. International workshop TYPES '95, Torino, Italy, June 5--8, 1995. Selected papers
The articles of mathematical interest will be reviewed individually. The workshop TYPES '94 has been announced (see Zbl 0866.00037). Indexed articles: \textit{Barthe, Gilles}, Implicit coercions in type systems, 1-15 [Zbl 1434.03081] \textit{Barthe, Gilles; Ruys, Mark; Barendregt, Henk}, A two-level approach towards lean proof-checking, 16-35 [Zbl 1407.68431] \textit{Berger, U.; Schwichtenberg, H.}, The greatest common divisor: a case study for program extraction from classical proofs, 36-46 [Zbl 1434.03024] \textit{Beylin, Ilya; Dybjer, Peter}, Extracting a proof of coherence for monoidal categories from a proof of normalization for monoids, 47-61 [Zbl 1407.68432] \textit{Cederquist, Jan; Negri, Sara}, A constructive proof of the Heine-Borel covering theorem for formal reals, 62-75 [Zbl 1434.03141] \textit{Coquand, Thierry; Smith, Jan M.}, An application of constructive completeness, 76-84 [Zbl 1434.03098] \textit{Cornes, Cristina; Terrasse, Delphine}, Automating inversion of inductive predicates in Coq, 85-104 [Zbl 1407.68433] \textit{Curmin, Philippe}, First order marked types, 105-119 [Zbl 1434.03027] \textit{Dybjer, Peter}, Internal type theory, 120-134 [Zbl 1434.03149] \textit{Giménez, Eduardo}, An application of co-inductive types in Coq: verification of the alternating bit protocol, 135-152 [Zbl 1407.68435] \textit{Hofmann, Martin}, Conservativity of equality reflection over intensional type theory, 153-164 [Zbl 1434.03038] \textit{Honsell, Furio; Miculan, Marino}, A natural deduction approach to dynamic logic, 165-182 [Zbl 1434.03084] \textit{Magnusson, Lena}, An algorithm for checking incomplete proof objects in type theory with localization and unification, 183-200 [Zbl 1407.68438] \textit{Padovani, Vincent}, Decidability of all minimal models, 201-215 [Zbl 1434.03056] \textit{Paulin-Mohring, Christine}, Circuits as streams in Coq: verification of a sequential multiplier, 216-230 [Zbl 1407.68439] \textit{Ranta, Aarne}, Context-relative syntactic categories and the formalization of mathematical text, 231-248 [Zbl 1434.03079] \textit{Stefanova, M.; Geuvers, H.}, A simple model construction for the calculus of constructions, 249-264 [Zbl 1434.03046] \textit{Tammet, Tanel; Smith, Jan M.}, Optimized encodings of fragments of type theory in first order logic, 265-287 [Zbl 1434.03033] \textit{von Plato, Jan}, Organization and development of a constructive axiomatization, 288-296 [Zbl 1434.03145]
- Types for proofs and programs. International workshop TYPES '96, Aussois, France, December 15--19, 1996. Selected papers
- TYPES '93, Types for proofs and programs. International Workshop, Nijmegen, the Netherlands, May 24-28, 1993. Selected papers
- -calculus in (Co)inductive-type theory
- Types for proofs and programs. 3rd international workshop, TYPES '99, Lökeberg, Sweden, June 12--16, 1999. Selected papers
- scientific article; zbMATH DE number 6904771 (Why is no real title available?)
- scientific article; zbMATH DE number 5309222 (Why is no real title available?)
- MODELS OF MARTIN-LÖF TYPE THEORY FROM ALGEBRAIC WEAK FACTORISATION SYSTEMS
- Types in compilation. 3rd international workshop, TIC 2000, Montreal, Canada, September 21, 2000. Revised selected papers
- (, 1)-categorical comprehension schemes
- Calculi, types and applications: essays in honour of M. Coppo, M. Dezani-Ciancaglini and S. Ronchi della Rocca
This page was built for publication: Types for proofs and programs. International workshop TYPES '95, Torino, Italy, June 5--8, 1995. Selected papers
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1815797)
