Treffer: A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance
Title:
A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance
Authors:
Source:
Lecture Notes in Computer Science ISBN: 9783642022722
Logical Methods in Computer Science, Vol Volume 7, Issue 2 (2011)
Logical Methods in Computer Science, Vol Volume 7, Issue 2 (2011)
Publication Status:
Preprint
Publisher Information:
Centre pour la Communication Scientifique Directe (CCSD), 2009.
Publication Year:
2009
Subject Terms:
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Corollary, Mathematical proof, 02 engineering and technology, 01 natural sciences, computer science - logic in computer science, Singleton, Logic Programming and Knowledge Representation, Pregnancy, 0202 electrical engineering, electronic engineering, information engineering, Modular design, Lambda calculus, Nonmonotonic Reasoning, BC1-199, Ecology, f.4.1, Discrete mathematics, Programming language, Algorithm, Computational Theory and Mathematics, Soundness, Physical Sciences, F.4.1, Program Analysis and Verification Techniques, Type (biology), Logic, Geometry, 0102 computer and information sciences, Type Inference, Mathematical analysis, Model Checking, Theoretical computer science, Artificial Intelligence, FOS: Mathematics, Genetics, Biology, Type theory, Semantics (computer science), QA75.5-76.95, Computer science, Logic in Computer Science (cs.LO), Completeness (order theory), Electronic computers. Computer science, FOS: Biological sciences, Computer Science, Proof complexity, Dependent type, Mathematics, Formal Methods in Software Verification and Control
Document Type:
Fachzeitschrift
Article<br />Part of book or chapter of book<br />Other literature type
File Description:
application/pdf
Language:
English
ISSN:
1860-5974
DOI:
10.2168/lmcs-7(2:4)2011
DOI:
10.1007/978-3-642-02273-9_3
DOI:
10.60692/8m3gz-8s552
DOI:
10.48550/arxiv.1102.2405
DOI:
10.60692/fydtc-cxj83
Access URL:
https://lmcs.episciences.org/1069/pdf
http://arxiv.org/pdf/1102.2405.pdf
http://arxiv.org/abs/1102.2405
https://doaj.org/article/f75592f46fb742aa827244554dc6a09f
https://research.chalmers.se/en/publication/111157
https://link.springer.com/chapter/10.1007/978-3-642-02273-9_3
https://www.tcs.ifi.lmu.de/~abel/lmcs10.pdf
https://core.ac.uk/display/21747331
https://rd.springer.com/chapter/10.1007/978-3-642-02273-9_3
http://www.tcs.ifi.lmu.de/~abel/lmcs10.pdf
https://ui.adsabs.harvard.edu/abs/2011arXiv1102.2405A/abstract
https://arxiv.org/abs/1102.2405
https://arxiv.org/pdf/1102.2405
http://arxiv.org/pdf/1102.2405.pdf
http://arxiv.org/abs/1102.2405
https://doaj.org/article/f75592f46fb742aa827244554dc6a09f
https://research.chalmers.se/en/publication/111157
https://link.springer.com/chapter/10.1007/978-3-642-02273-9_3
https://www.tcs.ifi.lmu.de/~abel/lmcs10.pdf
https://core.ac.uk/display/21747331
https://rd.springer.com/chapter/10.1007/978-3-642-02273-9_3
http://www.tcs.ifi.lmu.de/~abel/lmcs10.pdf
https://ui.adsabs.harvard.edu/abs/2011arXiv1102.2405A/abstract
https://arxiv.org/abs/1102.2405
https://arxiv.org/pdf/1102.2405
Rights:
CC BY ND
Springer TDM
arXiv Non-Exclusive Distribution
URL: https://arxiv.org/licenses/nonexclusive-distrib/1.0
Springer TDM
arXiv Non-Exclusive Distribution
URL: https://arxiv.org/licenses/nonexclusive-distrib/1.0
Accession Number:
edsair.doi.dedup.....c048a912e49f2d4396ed12a11fbb6e4a
Database:
OpenAIRE
Weitere Informationen
We define a logical framework with singleton types and one universe of small types. We give the semantics using a PER model; it is used for constructing a normalisation-by-evaluation algorithm. We prove completeness and soundness of the algorithm; and get as a corollary the injectivity of type constructors. Then we give the definition of a correct and complete type-checking algorithm for terms in normal form. We extend the results to proof-irrelevant propositions.