Types for Proofs and Programs
Subtitle: International Workshop, TYPES '98, Kloster Irsee, Germany, March 27-31, 1998, Selected Papers (Lecture Notes in Computer Science)
Contributors: Thorsten Altenkirch (Editor); Wolfgang Naraschewski (Editor); Bernhard Reus (Editor)
Edition: 1 edition
Publisher: Springer
Published: October 29, 1999
Language: eng
Format: Paperback
Number of pages: 207
ISBN-13: 9783540665373
Subjects: General Theory of Computing; Programming languages; Logic; Computer programming; General; Logic Design; Philosophy Of Mathematics; Computer Logic; Computers; Computers - Languages / Programming; Computer Books: Languages; Congresses; Programming - General; Computers / Logic Design; Formal Verification; Program Semantics; Proof Theory; Type Systems; Automatic theorem proving; Computer Science; Type theory
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>