TYPES 1993: Nijmegen, The Netherlands

Henk Barendregt, Tobias Nipkow (Eds.): Types for Proofs and Programs, International Workshop TYPES'93, Nijmegen, The Netherlands, May 24-28, 1993, Selected Papers. Lecture Notes in Computer Science 806 Springer 1994, ISBN 3-540-58085-9

Thorsten Altenkirch:
Proving Strong Normalization of CC by Modifying Realizability Semantics. 3-18
L. S. van Benthem Jutting, James McKinna, Robert Pollack:
Checking Algorithms for Pure Type Systems. 19-61
Thierry Coquand:
Infinite Objects in Type Theory. 62-78
Herman Geuvers:
Conservativity between Logics and Typed lambda Calculi. 79-107
Susumu Hayashi:
Logic of Refinement Types. 108-126
Leen Helmink, M. P. A. Sellink, Frits W. Vaandrager:
Proof-Checking a Data Link Protocol. 127-165
Martin Hofmann:
Elimination of Extensionality in Martin-Löf Type Theory. 166-190
François Leclerc, Christine Paulin-Mohring:
Programming with Streams in Coq - A Case Study: the Sieve of Eratosthenes. 191-212
Lena Magnusson, Bengt Nordström:
The ALF Proof Editor and Its Proof Engine. 213-237
Savi Maharaj:
Encoding Z-style Schemas in Type Theory. 238-262
Marino Miculan:
The Expressive Power of Structural Operational Semantics with Explicit Assumptions. 263-290
Catherine Parent:
Developing Certified Programs in the System Coq - The Program Tactic. 291-312
Randy Pollack:
Closure Under Alpha-Conversion. 313-332
Christophe Faffalli:
Machine Deduction. 333-351
Aarne Ranta:
Type Theory and the Informal Language of Mathematics. 352-365
David A. Wolfram:
Semantics for Abstract Clauses. 366-383

Last update Sat May 18 19:52:07 2013 CET by the DBLP Team —

Data released under the ODC-BY 1.0 license — See also our legal information page