What do you think?
Rate this book
Types for Proofs and Programs: International Workshop TYPES '93, Nijmegen, The Netherlands, May 24 - 28, 1993. Selected Papers
Proving strong normalization of CC by modifying realizability semantics.- Checking algorithms for Pure Type Systems.- Infinite objects in type theory.- Conservativity between logics and typed ? calculi.- Logic of refinement types.- Proof-checking a data link protocol.- Elimination of extensionality in Martin-Löf type theory.- Programming with streams in Coq a case The Sieve of Eratosthenes.- The Alf proof editor and its proof engine.- Encoding Z-style Schemas in type theory.- The expressive power of Structural Operational Semantics with explicit assumptions.- Developing certified programs in the system Coq the program tactic.- Closure under alpha-conversion.- Machine Deduction.- Type theory and the informal language of mathematics.- Semantics for abstract clauses.
400 pages, Paperback
Published March 12, 2014
Ratings & Reviews
Friends & Following
Create a free account to discover what your friends think of this book!
Community Reviews
No one has reviewed this book yet.