ISBN-10:
3540651373
ISBN-13:
9783540651376
Pub. Date:
11/13/1998
Publisher:
Springer Berlin Heidelberg
Types for Proofs and Programs: International Workshop TYPES'96, Aussois, France, December 15-19, 1996 Selected Papers / Edition 1

Types for Proofs and Programs: International Workshop TYPES'96, Aussois, France, December 15-19, 1996 Selected Papers / Edition 1

Paperback

Current price is , Original price is $109.0. You
Select a Purchase Option (1998)
  • purchase options
    $73.48 $109.00 Save 33% Current price is $73.48, Original price is $109. You Save 33%.
  • purchase options

Product Details

ISBN-13: 9783540651376
Publisher: Springer Berlin Heidelberg
Publication date: 11/13/1998
Series: Lecture Notes in Computer Science , #1512
Edition description: 1998
Pages: 380
Product dimensions: 6.10(w) x 9.25(h) x 0.03(d)

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.

Customer Reviews

Most Helpful Customer Reviews

See All Customer Reviews