Types for Proofs and Programs [electronic resource] : International Workshop, TYPES 2000, Durham, UK, December 8-12, 2000. Selected Papers /
Material type: TextSeries: Lecture Notes in Computer Science ; 2277Publisher: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2002Edition: 1st ed. 2002Description: VIII, 248 p. online resourceContent type:- text
- computer
- online resource
- 9783540458425
- Computer science
- Computer systems
- Mathematical logic
- Machine theory
- Compilers (Computer programs)
- Artificial intelligence
- Computer Science Logic and Foundations of Programming
- Computer System Implementation
- Mathematical Logic and Foundations
- Formal Languages and Automata Theory
- Compilers and Interpreters
- Artificial Intelligence
- 004.0151 23
- QA75.5-76.95
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.
There are no comments on this title.