Incorporating quotation and evaluation into Church's type theory: syntax and semantics

DOI10.1007/978-3-319-42547-4_7MaRDI QIDQ2817296zbMATH OpenOpenAlexFDO

Authors William M. Farmer

Publication date 30 August 2016

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1605.07068

Mathematics Subject Classification ID

Theory of programming languages (68N15)

Abstract: ${msmallCTT}_{mqe}$ is a version of Church's type theory that includes quotation and evaluation operators that are similar to quote and eval in the Lisp programming language. With quotation and evaluation it is possible to reason in ${msmallCTT}_{mqe}$ about the interplay of the syntax and semantics of expressions and, as a result, to formalize syntax-based mathematical algorithms. We present the syntax and semantics of ${msmallCTT}_{mqe}$ and give several examples that illustrate the usefulness of having quotation and evaluation in ${msmallCTT}_{mqe}$. We do not give a proof system for ${msmallCTT}_{mqe}$, but we do sketch what a proof system could look like.

Recommendations

• Incorporating quotation and evaluation into Church's type theory
• Theory morphisms in Church's type theory with quotation and evaluation
• HOL Light QE
• Ratio and Product Type Exponential Estimators of Population Mean in Double Sampling for Stratification
• Axiomatizing the quote

Cites work

• scientific article; zbMATH DE number 1926640 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• scientific article; zbMATH DE number 6296049 (Why is no real title available?)
• A formulation of the simple theory of types
• A reflective functional language for hardware design and theorem proving
• An introduction to mathematical logic and type theory: To truth through proof.
• Completeness in the theory of types
• Dependently typed programming in Agda
• Directly reflective meta-programming
• Explicit substitutions
• HOL Light: An Overview
• MetaML and multi-stage programming with explicit annotations
• The formalization of syntax-based mathematical algorithms using quotation and evaluation

Cited in

(7)

• Logic in quotes
• Incorporating quotation and evaluation into Church's type theory
• Ratio and Product Type Exponential Estimators of Population Mean in Double Sampling for Stratification
• The formalization of syntax-based mathematical algorithms using quotation and evaluation
• Theory morphisms in Church's type theory with quotation and evaluation
• HOL Light QE
• Formalizing mathematical knowledge as a biform theory graph: a case study

Describes a project that uses

Uses Software

• reFLect
• Agda
• MetaOCaml
• HOL Light
• ETPS
• HOL
• ML
• Coq

This page was built for publication: Incorporating quotation and evaluation into Church's type theory: syntax and semantics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2817296)