Types for proofs and programs. International workshop TYPES '95, Torino, Italy, June 5--8, 1995. Selected papers (Q1815797)

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]