Title: Types for proofs and programs
Description: Types for Proofs and Programs: International Workshop, TYPES’ 98 Kloster Irsee, Germany, March 27–31, 1998 Selected Papers<br />Author: Thorsten Altenkirch, Bernhard Reus, Wolfgang Naraschewski<br /> Published by Springer Berlin Heidelberg<br /> ISBN: 978-3-540-66537-3<br /> DOI: 10.1007/3-540-48167-2<br /><br />Table of Contents:<p></p><ul><li>On Relating Type Theories and Set Theories
</li><li>Communication Modelling and Context-Dependent Interpretation: An Integrated Approach
</li><li>Gröbner Bases in Type Theory
</li><li>A Modal Lambda Calculus with Iteration and Case Constructs
</li><li>Proof Normalization Modulo
</li><li>Proof of Imperative Programs in Type Theory
</li><li>An Interpretation of the Fan Theorem in Type Theory
</li><li>Conjunctive Types and SKInT
</li><li>Modular Structures as Dependent Types in Isabelle
</li><li>Metatheory of Verification Calculi in LEGO
</li><li>Bounded Polymorphism for Extensible Objects
</li><li>About Effective Quotients in Constructive Type Theory
</li><li>Algorithms for Equality and Unification in the Presence of Notational Definitions
</li><li>A Preview of the Basic Picture: A New Perspective on Formal Topology</li></ul>
Subjects: Type theory, Congresses, Computer programming, Automatic theorem proving, Logic, symbolic and mathematical, Computer science, Logic design, Artificial intelligence