| 1 |
Simple Type Theory with Undefinedness, Quotation, and Evaluation∗
|
|
|
|
In: http://imps.mcmaster.ca/doc/stt-with-uqe.pdf (2014)
|
|
Abstract:
This paper presents a version of simple type theory called Quqe0 that is based on Q0, the elegant formulation of Church’s type theory created and extensively studied by Peter B. Andrews. Quqe0 directly formalizes the traditional approach to undefinedness in which undefined expressions are treated as legitimate, nondenoting expressions that can be compo-nents of meaningful statements. Quqe0 is also equipped with a facility for reasoning about the syntax of expressions based on quotation and evalu-ation. Quotation is used to refer to a syntactic value that represents the syntactic structure of an expression, and evaluation is used to refer to the value of the expression that a syntactic value represents. With quotation and evaluation it is possible to reason in Quqe0 about the interplay of the syntax and semantics of expressions and, as a result, to formalize in Quqe0 syntax-based mathematical algorithms. The paper gives the syntax and semantics of Quqe0 as well as a proof system for Quqe0. The proof system is
|
|
Keyword:
Church’s type theory; evaluation; quotation; reasoning about syn- tax; substitution. ∗This research was supported by NSERC; truth predicates; undefinedness
|
|
URL: http://imps.mcmaster.ca/doc/stt-with-uqe.pdf
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.651.2532
|
|
BASE
|
|
Hide details
|
|
|
| 2 |
The Formalization of Syntax-Based Mathematical Algorithms Using Quotation and Evaluation?
|
|
|
|
In: http://imps.mcmaster.ca/doc/quote-eval.pdf (2013)
|
|
BASE
|
|
Show details
|
|
|
| 3 |
The Formalization of Syntax-Based Mathematical Algorithms Using Quotation and Evaluation ⋆
|
|
|
|
In: http://imps.mcmaster.ca/doc/quote-eval.pdf (2013)
|
|
BASE
|
|
Show details
|
|
|
| 4 |
Frameworks for reasoning about syntax that utilize quotation and evaluation
|
|
|
|
In: http://imps.mcmaster.ca/doc/syntax.pdf (2013)
|
|
BASE
|
|
Show details
|
|
|
| 5 |
Project EuDML--A First Year Demonstration
|
|
|
|
In: Intelligent Computer Mathematics ; Intelligent Computer Mathematics 18th Symposium, Calculemus 2011, and 10th International Conference, MKM 2011 ; https://hal.archives-ouvertes.fr/hal-00658076 ; Intelligent Computer Mathematics 18th Symposium, Calculemus 2011, and 10th International Conference, MKM 2011, Jul 2011, Bertinoro, Italy. pp.281-284, ⟨10.1007/978-3-642-22673-1_21⟩ (2011)
|
|
BASE
|
|
Show details
|
|
|
| 6 |
A Verified Compiler for Multithreaded PreScheme
|
|
|
|
In: http://repository.readscheme.org/ftp/papers/vlisp/mtps.ps.gz (1996)
|
|
BASE
|
|
Show details
|
|
|
|
|
