Types for proofs and programs. International workshop TYPES '95, Torino, Italy, June 5--8, 1995. Selected papers
type: Item
instance of: scholarly article
title: Types for proofs and programs. International workshop TYPES '95, Torino, Italy, June 5--8, 1995. Selected papers
zbMATH Open document ID: 0852.00045
DOI: 10.1007/3-540-61780-9
published in: Lecture Notes in Computer Science
publication date: 1996-11-19T00:00:00Z
review text: 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 categorie…
Mathematics Subject Classification ID: 00B25
Mathematics Subject Classification ID: 68-06
zbMATH DE Number: 947230
zbMATH Keywords: Types
zbMATH Keywords: Proofs
zbMATH Keywords: Programs
zbMATH Keywords: Workshop
zbMATH Keywords: Proceedings
zbMATH Keywords: Torino (Italy)
MaRDI profile type: Publication
full work available at URL: https://doi.org/10.1007/3-540-61780-9
OpenAlex ID: W4294254159
description: scientific article; zbMATH DE number 947230