Types for proofs and programs : International Workshop TYPES '94, Båstad, Sweden, June 6-10, 1994 : selected papers /
Enregistré dans:
| Collectivité auteur: | |
|---|---|
| Autres auteurs: | , , |
| Format: | Actes de congrès Livre |
| Langue: | English |
| Publié: |
Berlin ; New York :
Springer,
c1995.
|
| Collection: | Lecture notes in computer science ;
996. |
| Sujets: |
Table des matières:
- Communicating Contexts: a Pragmatic Approach to Information Exchange / Rene Ahn
- A Short and Flexible Proof of Strong Normalization for the Calculus of Constructions / Herman Geuvers
- Codifying Guarded Definitions with Recursive Schemes / Eduardo Gimenez
- The Metatheory of UTT / Healfdene Goguen
- A User's Friendly Syntax to Define Recursive Functions as Typed [lambda]-Terms / Pascal Manoury
- I/O Automata in Isabelle/HOL / Tobias Nipkow and Konrad Slind
- A Concrete Final Coalgebra Theorem for ZF Set Theory / Lawrence C. Paulson
- On Extensibility of Proof Checkers / Robert Pollack
- Syntactic Categories in the Language of Mathematics / Aarne Ranta
- Formalization of a [lambda]-Calculus with Explicit Substitutions in Coq / Amokrane Saibi.