ISBN-10:
3540617809
ISBN-13:
9783540617808
Pub. Date:
11/08/1996
Publisher:
Springer Berlin Heidelberg
Types for Proofs and Programs: International Workshop, TYPES '95, Torino, Italy, June 5 - 8, 1995 Selected Papers / Edition 1

Types for Proofs and Programs: International Workshop, TYPES '95, Torino, Italy, June 5 - 8, 1995 Selected Papers / Edition 1

by Stefano Berardi, Mario Coppo

Paperback

Current price is , Original price is $99.0. You
Select a Purchase Option (1996)
  • purchase options
    $79.91 $99.00 Save 19% Current price is $79.91, Original price is $99. You Save 19%.
  • purchase options

Product Details

ISBN-13: 9783540617808
Publisher: Springer Berlin Heidelberg
Publication date: 11/08/1996
Series: Lecture Notes in Computer Science , #1158
Edition description: 1996
Pages: 298
Product dimensions: 6.10(w) x 9.25(h) x 0.03(d)

Table of Contents

Implicit coercions in type systems.- A two-level approach towards lean proof-checking.- The greatest common divisor: A case study for program extraction from classical proofs.- Extracting a proof of coherence for monoidal categories from a proof of normalization for monoids.- A constructive proof of the Heine-Borel covering theorem for formal reals.- An application of constructive completeness.- Automating inversion of inductive predicates in Coq.- First order marked types.- Internal type theory.- An application of co-inductive types in Coq: Verification of the alternating bit prool.- Conservativity of equality reflection over intensional type theory.- A natural deduction approach to dynamic logic.- An algorithm for checking incomplete proof objects in type theory with localization and unification.- Decidability of all minimal models.- Circuits as streams in Coq: Verification of a sequential multiplier.- Context-relative syntactic categories and the formalization of mathematical text.- A simple model construction for the Calculus of Constructions.- Optimized encodings of fragments of type theory in first order logic.- Organization and development of a constructive axiomatization.

Customer Reviews

Most Helpful Customer Reviews

See All Customer Reviews