Types for Proofs and Programs

Types for Proofs and Programs: International Workshop, TYPES’ 98 Kloster Irsee, Germany, March 27–31, 1998 Selected PapersAuthor: Thorsten Altenkirch, Bernhard Reus, Wolfgang Naraschewski Published by Springer Berlin Heidelberg ISBN: 978-3-540-66537-3 DOI: 10.1007/3-540-48167-2Table of Contents:On Relating Type Theories and Set Theories
Communication Modelling and Context-Dependent Interpretation: 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 Picture: A New Perspective on Formal Topology