E-Book, Englisch, Band 2277, 248 Seiten, eBook
Callaghan / Luo / McKinna Types for Proofs and Programs
Erscheinungsjahr 2003
ISBN: 978-3-540-45842-5
Verlag: Springer
Format: PDF
Kopierschutz: 1 - PDF Watermark
International Workshop, TYPES 2000, Durham, UK, December 8-12, 2000. Selected Papers
E-Book, Englisch, Band 2277, 248 Seiten, eBook
Reihe: Lecture Notes in Computer Science
ISBN: 978-3-540-45842-5
Verlag: Springer
Format: PDF
Kopierschutz: 1 - PDF Watermark
Zielgruppe
Research
Autoren/Hrsg.
Weitere Infos & Material
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.
