×

Twenty-five years of constructive type theory. Proceedings of a congress, Venice, Italy, Ocober 19–21, 1995. (English) Zbl 0899.00026

Oxford Logic Guides. 36. Oxford: Clarendon Press. viii, 283 p. (1998).

Show indexed articles as search result.

The articles of this volume will be reviewed individually.
Indexed articles:
Baratella, Stefano; Berardi, Stefano, Yet another constructivization of classical logic, 1-20 [Zbl 0940.03065]
Betarte, Gustavo; Tasistro, Alvaro, Extension of Martin-Löf’s type theory with record types and subtyping, 21-39 [Zbl 0930.03088]
de Bruijn, Nicolaas Govert, Type-theoretical checking and philosophy of mathematics, 41-56 [Zbl 0947.03006]
Cederquist, Jan; Coquand, Thierry; Negri, Sara, The Hahn-Banach theorem in type theory, 57-72 [Zbl 0940.03069]
Coquand, Catarina, A realizability interpretation of Martin-Löf’s type theory, 73-82 [Zbl 0937.03068]
Hofmann, Martin; Streicher, Thomas, The groupoid interpretation of type theory, 83-111 [Zbl 0930.03089]
Mäenpää, Petri, Analytic program derivation in type theory, 113-126 [Zbl 0929.03038]
Martin-Löf, Per, An intuitionistic theory of types, 127-172 [Zbl 0931.03070]
Nour, Karim, On storage operators, 173-190 [Zbl 0930.03015]
Palmgren, Erik, On universes in type theory, 191-204 [Zbl 0930.03090]
Pollack, Robert, How to believe a machine-checked proof, 205-220 [Zbl 0936.03012]
Sambin, Giovanni; Valentini, Silvio, Building up a toolbox for Martin-Löf’s type theory: Subset theory, 221-244 [Zbl 0930.03091]
Setzer, Anton, An introduction to well-ordering proofs in Martin-Löf’s type theory, 245-263 [Zbl 0930.03092]
Tait, William W., Variable-free formalization of the Curry-Howard theory, 265-274 [Zbl 0930.03016]
Valentini, Silvio, The forget-restore principle: A paradigmatic example, 275-283 [Zbl 0937.03069]

MSC:

00B25 Proceedings of conferences of miscellaneous specific interest
03-06 Proceedings, conferences, collections, etc. pertaining to mathematical logic and foundations