Output details
11 - Computer Science and Informatics
Royal Holloway, University of London
Return to search
Output 0 of 0 in the submission
Article title
Classical Predicative Logic-Enriched Type Theories
Type
D - Journal article
Title of journal
Annals of Pure and Applied Logic
Article number
-
Volume number
161
Issue number
11
First page of article
1315
ISSN of journal
0168-0072
Year of publication
2010
Number of additional authors
1
Additional information
<11> This paper studies, for the first time, the meta-theoretic properties of the framework of Logic-enriched Type Theories, a novel approach that allows flexible treatment of various logics in type theory, including classical logics. For example, LTTs have been implemented in Plastic and used in formalisations of Weyl's predicative mathematics. The paper develops the meta-theory systematically and establishes the foundation of the implementation and applications of LTTs in proof assistants. It was supported by EPSRC grant GR/R84092 'Pythagoras: Machine support for semi-formalised proof oriented mathematics'.
Interdisciplinary
-
Cross-referral requested
-
Research group
C - Centre for Software Language Engineering
Citation count
0
Proposed double-weighted
No
Double-weighted statement
-
Reserve for a double-weighted output
No
Non-English
No
English abstract
-
