close
1.

図書
図書
1. Types for proofs and programs : International Workshop TYPES '98, Kloster Irsee, Germany, March 27-31, 1998 : selected papers
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
2.

図書
図書
2. Types for proofs and programs : International Workshop TYPES '96, Aussois, France, December 15-19, 1996 : selected papers
Eduardo Giménez, Christine Paulin-Mohring (eds.)
出版情報: Berlin ; Tokyo : Springer, c1998  viii, 372 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 1512
所蔵情報: loading…
3.

図書
図書
3. Types for proofs and programs : International Workshop TYPES '94, Båstad, Sweden, June 6-10, 1994 : selected papers (: gw)
Peter Dybjer, Bengt Nordström, Jan Smith (eds.)
出版情報: Berlin : Springer-Verlag, c1995  x, 202 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 996
所蔵情報: loading…
4.

図書
図書
4. Types for proofs and programs : International Workshop TYPES '95, Torino, Italy, June 5-8, 1995 : selected papers
Stefano Berardi, Mario Coppo, (eds.)
出版情報: Berlin ; New York : Springer, c1996  x, 296 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 1158
所蔵情報: loading…
5.

図書
図書
5. Types for proofs and programs : International Workshop TYPES '93, Nijmegen, The Netherlands, May 24-28, 1993 : selected papers (: gw ; : us)
Henk Barendregt, Tobias Nipkow, (eds.)
出版情報: Berlin ; Tokyo : Springer-Verlag, c1994  383 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 806
所蔵情報: loading…
6.

図書
図書
6. Types for proofs and programs : International Workshop, TYPES 2002, Berg en Dal, the Netherlands, April 24-28, 2002 : selected papers
Herman Geuvers, Freek Wiedijk (eds.)
出版情報: Berlin ; Tokyo : Springer, c2003  viii, 330 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 2646
所蔵情報: loading…
7.

図書
図書
7. Types for Proofs and Programs : International Workshop, TYPES 2000, Durham, UK, December 8-12, 2000 : selected papers
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
8.

図書
図書
8. Types for proofs and programs : International Workshop, TYPES '99, Lökeberg, Sweden, June 12-16, 1999 : selected papers
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
9.

図書
図書
9. Types for proofs and programs : International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, 2004 : revised selected papers
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…
10.

図書
図書
10. Types for proofs and programs : International Workshop, TYPES 2003, Torino, Italy, April 30 - May 4, 2003 : revised selected papers
Stefano Berardi, Mario Coppo, Ferruccio Damiani (eds.)
出版情報: Berlin ; Tokyo : Springer, c2004  x, 408 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 3085
所蔵情報: loading…
文献の複写および貸借の依頼を行う
 文献複写・貸借依頼