This volume contains thoroughly refereed and revised full papers selected from the presentations at the first workshop held under the auspices of the ESPRIT Basic Research Action 6453 Types for Proofs and Programs in Nijmegen, The Netherlands, in May 1993.
As the whole ESPRIT BRA 6453, this volume is devoted to the theoretical foundations, design and applications of systems for theory development. Such systems help in designing mathematical axiomatisation, performing computer-aided logical reasoning, and managing databases of mathematical facts; they are also known as proof assistants or proof checkers.
Author(s): Henk Barendregt, Tobias Nipkow (eds.)
Series: Lecture Notes in Computer Science 806
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 1994
Language: English
Pages: 395
Tags: Mathematical Logic and Formal Languages; Logics and Meanings of Programs; Artificial Intelligence (incl. Robotics)
Introduction....Pages 1-2
Proving strong normalization of CC by modifying realizability semantics....Pages 3-18
Checking algorithms for Pure Type Systems....Pages 19-61
Infinite objects in type theory....Pages 62-78
Conservativity between logics and typed λ calculi....Pages 79-107
Logic of refinement types....Pages 108-126
Proof-checking a data link protocol....Pages 127-165
Elimination of extensionality in Martin-Löf type theory....Pages 166-190
Programming with streams in Coq a case study: The Sieve of Eratosthenes....Pages 191-212
The Alf proof editor and its proof engine....Pages 213-237
Encoding Z-style Schemas in type theory....Pages 238-262
The expressive power of Structural Operational Semantics with explicit assumptions....Pages 263-290
Developing certified programs in the system Coq the program tactic....Pages 291-312
Closure under alpha-conversion....Pages 313-332
Machine Deduction....Pages 333-351
Type theory and the informal language of mathematics....Pages 352-365
Semantics for abstract clauses....Pages 366-383
