close
1.

図書

図書
Paul Callaghan ... [et al.] (eds.)
出版情報: Berlin ; New York : Springer, c2002  viii, 242 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 2277
所蔵情報: loading…
目次情報: 続きを見る
Collection Principles in Dependent Type Theory / Peter Aczel ; Nicola Gambino
Executing Higher Order Logic / Stefan Berghofer ; Tobias Nipkow
ATour with Constructive Real Numbers / Alberto Ciaffaglione ; Pietro Di Gianantonio
An Implementation of Type: Type / Thierry Coquand ; Makoto Takeyama
On the Logical Content of Computational Type Theory: A Solution to CurryÆs Problem / Matt Fairtlough ; Michael Mendler
Constructive Reals in Coq: Axioms and Categoricity / Herman Geuvers ; Milad Niqui
A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals / Freek Wiedijk ; Jan Zwanenburg
AKripke-Style Model for the Admissibility of Structural Rules / Healfdene Goguen
Towards Limit Computable Mathematics / Susumu Hayashi ; Masahiro Nakata
Formalizing the Halting Problem in a Constructive Type Theory / Kristofer Johannisson
On the Proofs of Some Formally Unprovable Propositions and Prototype Proofs in Type Theory / Giuseppe Longo
Changing Data Structures in Type Theory: AStudy of Natural Numbers / Nicolas Magaud ; Yves Bertot
Elimination with a Motive / Conor McBride
Generalization in Type Theory Based Proof Assistants / Olivier Pons
An Inductive Version of Nash-WilliamsÆ Minimal-Bad-Sequence Argument for HigmanÆs Lemma / Monika Seisenberger
Author Index
Collection Principles in Dependent Type Theory / Peter Aczel ; Nicola Gambino
Executing Higher Order Logic / Stefan Berghofer ; Tobias Nipkow
ATour with Constructive Real Numbers / Alberto Ciaffaglione ; Pietro Di Gianantonio
2.

図書

図書
Jean Christophe Filliâtre, Christine Paulin-Mohring, Benjamin Werner (eds.)
出版情報: Berlin : Springer, c2006  viii, 273 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 3839
所蔵情報: loading…
3.

図書

図書
Stefano Berardi, Mario Coppo, Ferruccio Damiani (eds.)
出版情報: Berlin ; Tokyo : Springer, c2004  x, 408 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 3085
所蔵情報: loading…
4.

図書

図書
Thierry Coquand ... [et al.] (eds.)
出版情報: Berlin ; New York : Springer, c2000  193 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 1956
所蔵情報: loading…
目次情報: 続きを見る
Specification and Verification of a Formal System for Structurally Recursive Functions / Andreas Abel
A Predicative Strong Normalisation Proof for a ?-Calculus with Interleaving Inductive Types / Thorsten Altenkirch
Polymorphic Intersection Type Assignment for Rewrite Systems with Abstraction and ?-Rule / Steffen van Bakel ; Franco Barbanera ; Maribel Fernandez
Computer-Assisted Mathematics at Work (The Hahn-Banach Theorem in Isabelle/Isar) / Gertrud Bauer ; Markus Wenzel
Specification of a Smart Card Operating System / Gustavo Betarte ; Cristina Cornes ; Nora Szasz ; Alvaro Tasistro
Implementation Techniques for Inductive Types in Plastic / Paul Callaghan ; Zhaohui Luo
A Co-inductive Approach to Real Numbers / Alberto Ciaffaglione ; Pietro Di Gianantonio
Information Retrieval in a Coq Proof Library Using Type Isomorphisms / David Delahaye
Memory Management: An Abstract Formulation of Incremental Tracing / Healfdene Goguen ; Richard Brooksby ; Rod Burstall
The Three Gap Theorem (Steinhaus Conjecture) / Micaela Mayero
Formalising Formulas-as-Types-as-Objects / Qiao Haiyan
Author Index
Specification and Verification of a Formal System for Structurally Recursive Functions / Andreas Abel
A Predicative Strong Normalisation Proof for a ?-Calculus with Interleaving Inductive Types / Thorsten Altenkirch
Polymorphic Intersection Type Assignment for Rewrite Systems with Abstraction and ?-Rule / Steffen van Bakel ; Franco Barbanera ; Maribel Fernandez
5.

図書

図書
Herman Geuvers, Freek Wiedijk (eds.)
出版情報: Berlin ; Tokyo : Springer, c2003  viii, 330 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 2646
所蔵情報: loading…
文献の複写および貸借の依頼を行う
 文献複写・貸借依頼