Types for Proofs and Programs: International Workshop, TYPES '98, Kloster Irsee, Germany, March 27-31, 1998, Selected Papers

by Thorsten Altenkirch (Editor)

On Relating Type Theories and Set Theories.- Communication Modelling and Context-Dependent An Integrated Approach.- Gröbner Bases in Type Theory.- A Modal Lambda Calculus with Iteration and Case Constructs.- Proof Normalization Modulo.- Proof of Imperative Programs in Type Theory.- An Interpretation of the Fan Theorem in Type Theory.- Conjunctive Types and SKInT.- Modular Structures as Dependent Types in Isabelle.- Metatheory of Verification Calculi in LEGO.- Bounded Polymorphism for Extensible Objects.- About Effective Quotients in Constructive Type Theory.- Algorithms for Equality and Unification in the Presence of Notational Definitions.- A Preview of the Basic A New Perspective on Formal Topology.

220 pages, Paperback

Published March 12, 2014