1 option
Types for Proofs and Programs : International Workshop, TYPES 2000, Durham, UK, December 8-12, 2000. Selected Papers / edited by Paul Callaghan, Zhaohui Luo, James McKinna, Robert Pollack.
LIBRA Q341 .P7 2004
Available from offsite location
- Format:
- Book
- Series:
- Computer Science (Springer-11645)
- Lecture notes in computer science 0302-9743 ; 2277.
- Lecture Notes in Computer Science, 0302-9743 ; 2277
- Language:
- English
- Subjects (All):
- Computer logic.
- Computer architecture.
- Logic, Symbolic and mathematical.
- Programming languages (Electronic computers).
- Artificial intelligence.
- Logics and Meanings of Programs.
- Computer System Implementation.
- Mathematical Logic and Foundations.
- Mathematical Logic and Formal Languages.
- Programming Languages, Compilers, Interpreters.
- Artificial Intelligence.
- Local Subjects:
- Logics and Meanings of Programs.
- Computer System Implementation.
- Mathematical Logic and Foundations.
- Mathematical Logic and Formal Languages.
- Programming Languages, Compilers, Interpreters.
- Artificial Intelligence.
- Physical Description:
- 1 online resource (VIII, 248 pages).
- Edition:
- First edition 2002.
- Contained In:
- Springer eBooks
- Place of Publication:
- Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2002.
- System Details:
- text file PDF
- Contents:
- 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.
- Other Format:
- Printed edition:
- ISBN:
- 978-3-540-45842-5
- 9783540458425
- Access Restriction:
- Restricted for use by site license.
The Penn Libraries is committed to describing library materials using current, accurate, and responsible language. If you discover outdated or inaccurate language, please fill out this feedback form to report it and suggest alternative language.