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.

図書

図書
Thorsten Altenkirch, Wolfgang Naraschewski, Bernhard Reus (eds.)
出版情報: Berlin ; Tokyo : Springer, c1999  viii, 207 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 1657
所蔵情報: loading…
目次情報: 続きを見る
On Relating Type Theories and Set Theories / Peter Aczel
Communication Modelling and Context-Dependent Interpretation: An Integrated Approach / René Ahn ; Tijn Borghuis
Gröbner Bases in Type Theory / Thierry Coquand ; Henrik Persson
A Modal Lambda Calculus with Iteration and Case Constructs / Joëlle Despeyroux ; Pierre Leleu
Proof Normalization Modulo / Gilles Dowek ; Benjamin Werner
Proof of Imperative Programs in Type Theory / Jean-Christophe Filliâtre
An Interpretation of the Fan Theoremin Type Theory / Daniel Fridlender
Conjunctive Types and SKInT / Jean Goubault-Larrecq
Modular Structures as Dependent Types in Isabelle / Florian Kammüller
Metatheory of Verification Calculi in LEGO / Thomas Kleymann
Bounded Polymorphism for Extensible Objects / Luigi Liquori
About Effective Quotients in Constructive Type Theory / Maria Emilia Maietti
Algorithms for Equality and Unification in the Presence of Notational Definitions / Frank Pfenning ; Carsten Schurmann
A Preview of the Basic Picture: A New Perspective on Formal Topology / Giovanni Sambin ; Silvia Gebellato
On Relating Type Theories and Set Theories / Peter Aczel
Communication Modelling and Context-Dependent Interpretation: An Integrated Approach / René Ahn ; Tijn Borghuis
Gröbner Bases in Type Theory / Thierry Coquand ; Henrik Persson
4.

図書

図書
Eduardo Giménez, Christine Paulin-Mohring (eds.)
出版情報: Berlin ; Tokyo : Springer, c1998  viii, 372 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 1512
所蔵情報: loading…
5.

図書

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

図書

図書
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
7.

図書

図書
Herman Geuvers, Freek Wiedijk (eds.)
出版情報: Berlin ; Tokyo : Springer, c2003  viii, 330 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 2646
所蔵情報: loading…
8.

図書

図書
Stefano Berardi, Mario Coppo, (eds.)
出版情報: Berlin ; New York : Springer, c1996  x, 296 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 1158
所蔵情報: loading…
9.

図書

図書
Peter Dybjer, Bengt Nordström, Jan Smith (eds.)
出版情報: Berlin : Springer-Verlag, c1995  x, 202 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 996
所蔵情報: loading…
10.

図書

図書
Henk Barendregt, Tobias Nipkow, (eds.)
出版情報: Berlin ; Tokyo : Springer-Verlag, c1994  383 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 806
所蔵情報: loading…
文献の複写および貸借の依頼を行う
 文献複写・貸借依頼