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

DOI10.1007/978-3-319-42547-4_7zbMATH Open1344.68204arXiv1605.07068OpenAlexW2962936422MaRDI QIDQ2817296FDOQ2817296

Authors: William M. Farmer 

Publication date: 30 August 2016

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

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.

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

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

Mathematics Subject Classification ID

Theory of programming languages (68N15)

Cites Work

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

Cited In (7)

• Logic in quotes
• Ratio and Product Type Exponential Estimators of Population Mean in Double Sampling for Stratification
• Incorporating quotation and evaluation into Church's type theory
• 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

Uses Software

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

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)