Types for Proofs and Programs

International Workshop, TYPES 2000, Durham, UK, December 8-12, 2000. Selected Papers

256 Seiten, Taschenbuch

Kurzbeschreibung des Verlags

Collection Principles in Dependent Type Theory.- Executing Higher Order Logic.- A Tour with Constructive Real Numbers.- An Implementation of Type:Type.- On the Logical Content of Computational Type Theory: A Solution to Curry's Problem.- Constructive Reals in Coq: Axioms and Categoricity.- A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals.- A Kripke-Style Model for the Admissibility of Structural Rules.- Towards Limit Computable Mathematics.- Formalizing the Halting Problem in a Constructive Type Theory.- On the Proofs of Some Formally Unprovable Propositions and Prototype Proofs in Type Theory.- Changing Data Structures in Type Theory: A Study of Natural Numbers.- Elimination with a Motive.- Generalization in Type Theory Based Proof Assistants.- An Inductive Version of Nash-Williams' Minimal-Bad-Sequence Argument for Higman's Lemma.

• Reihe: Lecture Notes in Computer Science
• Themen: Informatik und Informationstechnologie Informatik Künstliche Intelligenz (KI)
• ISBN: 9783540432876
• Sprache: Englisch
• Erscheinungsdatum: 20.02.2002
• Größe: 235 x 155 mm
• Verlag: Springer
• Herausgegeben von: Zhaohui Luo, Paul Callaghan, Robert Pollack, James McKinna