Types for Proofs and Programs International Workshop TYPES'96, Aussois, France, December 15-19, 1996 Selected Papers / edited by Eduardo Gimenez, Christine Paulin-Mohring.

This book constitutes the thoroughly revised post-workshop proceedings of the first annual workshop held under the auspices of the ESPRIT Working Group 21900 TYPES in Aussois, France in December 1996. The 18 revised full papers presented in the book were carefully reviewed and selected from the 30 p...

Full description

Saved in:

Bibliographic Details
Corporate Author:	SpringerLink (Online service)
Other Authors:	Gimenez, Eduardo (Editor), Paulin-Mohring, Christine (Editor)
Format:	eBook
Language:	English
Published:	Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 1998.
Edition:	1st ed. 1998.
Series:	Lecture Notes in Computer Science, 1512 Springer eBook Collection.
Subjects:	Software engineering. Computer logic. Mathematical logic. Programming languages (Electronic computers). Artificial intelligence. Electronic resources (E-books)
Online Access:	Click to view e-book
Holy Cross Note:	Loaded electronically. Electronic access restricted to members of the Holy Cross Community.

Table of Contents:

Coercion synthesis in computer implementations of type-theoretic frameworks
Verification of the interface of a small proof system in coq
An implementation of the Heine-Borel covering theorem in type theory
Detecting and removing dead-code using rank 2 intersection
A type-free formalization of mathematics where proofs are objects
Higman's lemma in type theory
A proof of weak termination of typed ??-calculi
Proof style
Some algorithmic and proof-theoretical aspects of coercive subtyping
Semantical BNF
The internal type theory of a Heyting pretopos
Inverting inductively defined relations in LEGO
A generic normalisation proof for pure type systems
Proving a real time algorithm for ATM in Coq
Dependent types with explicit substitutions: A meta-theoretical development
Type inference verified: Algorithm W in Isabelle/HOL
Continuous lattices in formal topology
Abstract insertion sort in an extension of type theory with record types and subtyping.

Types for Proofs and Programs International Workshop TYPES'96, Aussois, France, December 15-19, 1996 Selected Papers / edited by Eduardo Gimenez, Christine Paulin-Mohring.

Similar Items