Types for Proofs and Programs : International Workshop, TYPES 2000, Durham, UK, December 8-12, 2000 : selected papers

>> Google Books

所蔵情報QRコード

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 <BA00009279>

著者名:

ISBN:

9783540432876 [3540432876]

書誌ID:

BA55870093

子書誌情報

フルテキスト

所蔵情報

他の版・巻

書誌詳細

注記:

Includes bibliographies and index

主題:

Automatic theorem proving--Congresses; Computer programming--Congresses; Type theory--Congresses

言語:

英語

目次情報:

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

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

続きを見る

東工大ブックレビュー

類似資料:

1 図書 Types for proofs and programs : International Workshop, TYPES '99, Lökeberg, Sweden, June 12-16, 1999 : selected papers International Workshop on TYPES, Coquand, Thierry, 1961- Springer	7 図書 Types for proofs and programs : International Workshop TYPES '95, Torino, Italy, June 5-8, 1995 : selected papers International Workshop on TYPES, Berardi, Stefano, Coppo, Mario Springer
2 図書 Types for proofs and programs : International Workshop TYPES '96, Aussois, France, December 15-19, 1996 : selected papers International Workshop on TYPES, Giménez, Eduardo, 1967-, Paulin-Mohring, Christine, 1962- Springer	8 図書 Types for proofs and programs : International Workshop TYPES '94, Båstad, Sweden, June 6-10, 1994 : selected papers (: gw) International Workshop on TYPES, Dybjer, Peter, Nordström, Bengt, Smith, Jan M Springer-Verlag
3 図書 Types for proofs and programs : International Workshop TYPES '98, Kloster Irsee, Germany, March 27-31, 1998 : selected papers International Workshop on TYPES, Altenkirch, Thorsten, 1962-, Naraschewski, Wolfgang, 1970-, Reus, Bernhard, 1965- Springer	9 図書 Types for proofs and programs : International Workshop TYPES '93, Nijmegen, The Netherlands, May 24-28, 1993 : selected papers (: gw ; : us) International Workshop on TYPES, Barendregt, H. P. (Hendrik Pieter), 1947-, Nipkow, Tobias, 1958- Springer-Verlag
4 図書 Types for proofs and programs : International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, 2004 : revised selected papers International Workshop on TYPES, Filliâtre, Jean-Christophe, Paulin-Mohring, Christine, 1962-, Werner, Benjamin Springer	10 図書 Automata, languages and programming : 28th International Colloquium, ICALP 2001, Crete, Greece, July 8-12, 2001 : proceedings International Colloquium on Automata, Languages and Programming, Orejas, Fernando, Spirakis, P. G. (Paul G.), 1955-, … Springer
5 図書 Types for proofs and programs : International Workshop, TYPES 2002, Berg en Dal, the Netherlands, April 24-28, 2002 : selected papers International Workshop on TYPES, Geuvers, Herman, 1964-, Wiedijk, Freek, 1961- Springer	11 電子ブック Types for Proofs and Programs TYPES 2000, Callaghan, Paul SpringerLink Books - AutoHoldings, Springer Berlin Heidelberg
6 図書 Types for proofs and programs : International Workshop, TYPES 2003, Torino, Italy, April 30 - May 4, 2003 : revised selected papers International Workshop on TYPES, Berardi, Stefano, Coppo, Mario, Damiani, Ferruccio Springer	12 図書 Global computing : IST/FET International Workshop, GC 2004, Rovereto, Italy, March 9-12, 2004 : revised selected papers International Workshop on Global Computing, Priami, Corrado, Quaglia, Paola Springer