Types for Proofs and Programs, International Workshop TYPES 93, Nijmegen, The Netherlands, May 24-28, 1993, Selected Papers - researchr publication

researchr

You are not signed in
Sign in
Sign up

Henk Barendregt, Tobias Nipkow, editors, Types for Proofs and Programs, International Workshop TYPES 93, Nijmegen, The Netherlands, May 24-28, 1993, Selected Papers. Volume 806 of Lecture Notes in Computer Science, Springer, 1994.

Conference: TYPES1994

Abstract is missing.

Proving Strong Normalization of CC by Modifying Realizability SemanticsThorsten Altenkirch. 3-18

Checking Algorithms for Pure Type SystemsL. S. van Benthem Jutting, James McKinna, Robert Pollack. 19-61

Infinite Objects in Type TheoryThierry Coquand. 62-78

Conservativity between Logics and Typed lambda CalculiHerman Geuvers. 79-107

Logic of Refinement TypesSusumu Hayashi. 108-126

Proof-Checking a Data Link ProtocolLeen Helmink, M. P. A. Sellink, Frits W. Vaandrager. 127-165

Elimination of Extensionality in Martin-Löf Type TheoryMartin Hofmann. 166-190

Programming with Streams in Coq - A Case Study: the Sieve of EratosthenesFrançois Leclerc, Christine Paulin-Mohring. 191-212

The ALF Proof Editor and Its Proof EngineLena Magnusson, Bengt Nordström. 213-237

Encoding Z-style Schemas in Type TheorySavi Maharaj. 238-262

The Expressive Power of Structural Operational Semantics with Explicit AssumptionsMarino Miculan. 263-290

Developing Certified Programs in the System Coq - The Program TacticCatherine Parent. 291-312

Closure Under Alpha-ConversionRandy Pollack. 313-332

Machine DeductionChristophe Faffalli. 333-351

Type Theory and the Informal Language of MathematicsAarne Ranta. 352-365

Semantics for Abstract ClausesDavid A. Wolfram. 366-383

runs on WebDSL