Incorporating quotation and evaluation into Church's type theory

DOI10.1016/J.IC.2018.03.001zbMATH Open1390.68168arXiv1612.02785OpenAlexW2581306138MaRDI QIDQ1753993FDOQ1753993

Authors: William M. Farmer 

Publication date: 30 May 2018

Published in: Information and Computation (Search for Journal in Brave)

Abstract: ${mCTT}_{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 ${mCTT}_{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 ${mCTT}_{mqe}$ as well as a proof system for ${mCTT}_{mqe}$. The proof system is shown to be sound for all formulas and complete for formulas that do not contain evaluations. We give several examples that illustrate the usefulness of having quotation and evaluation in ${mCTT}_{mqe}$.

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

Recommendations

• Incorporating quotation and evaluation into Church's type theory: syntax and semantics
• 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

zbMATH Keywords

evaluationreflectionsubstitutionsymbolic computationsimple type theoryschemasquotationmetareasoningChurch's type theorymeaning formulasquasiquotationreasoning about syntax

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Functional programming and lambda calculus (68N18)

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?)
• IMPS: An interactive mathematical proof system
• Dependently typed programming in Agda
• HOL Light QE
• Nominal logic, a first order theory of names and binding
• Axiomatic theories of truth
• Generic literals
• Title not available (Why is that?)
• A new approach to abstract syntax with variable binding
• A modal analysis of staged computation
• Title not available (Why is that?)
• Contextual modal type theory
• HOL Light: An Overview
• Title not available (Why is that?)
• Meta Reasoning in ACL2
• Completeness in the theory of types
• Proof synthesis and reflection for linear arithmetic
• Theorem Proving in Higher Order Logics
• The calculus of constructions
• Title not available (Why is that?)
• Proof by computation in the Coq system
• A simple type theory with partial functions and subtypes
• Automated Reasoning
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• \textit{Theorema}: Towards computer-aided mathematical theory exploration
• The Four Colour Theorem: Engineering of a Formal Proof
• Title not available (Why is that?)
• A machine-checked proof of the odd order theorem
• Certification of Automated Termination Proofs
• On reflection principles
• Automatic synthesis of typed \(\Lambda\)-programs on term algebras
• MetaML and multi-stage programming with explicit annotations
• A reflective functional language for hardware design and theorem proving
• Explicit substitutions
• The Impact of the Lambda Calculus in Logic and Computer Science
• Title not available (Why is that?)
• The seven virtues of simple type theory
• Staged computation with names and necessity
• Reflection in conditional rewriting logic
• Title not available (Why is that?)
• Directly reflective meta-programming
• Theorem Proving in Higher Order Logics
• A partial functions version of Church's simple theory of types
• Formalizing mathematical knowledge as a biform theory graph: a case study
• Title not available (Why is that?)
• Title not available (Why is that?)
• Axiomatizing the quote
• Typed self-interpretation by pattern matching
• Typed self-evaluation via intensional type functions
• Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages
• Theory morphisms in Church's type theory with quotation and evaluation
• Incorporating quotation and evaluation into Church's type theory: syntax and semantics
• Self-representation in Girard's System U
• Breaking through the normalization barrier: a self-interpreter for F-omega
• The formalization of syntax-based mathematical algorithms using quotation and evaluation
• Elaborator reflection: extending Idris in Idris
• Andrews' type theory with undefinedness
• Tactics for Reasoning Modulo AC in Coq
• Syntax for Free: Representing Syntax with Binding Using Parametricity
• IMPS: An updated system description
• MathScheme: project description
• Biform Theories in Chiron
• High-Level Theories

Cited In (6)

• Logic operators and quantifiers in type-theory of algorithms
• 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
• Incorporating quotation and evaluation into Church's type theory: syntax and semantics
• Theory morphisms in Church's type theory with quotation and evaluation
• HOL Light QE

Uses Software

• ACL2
• Coq
• Theorema
• ML
• MetaPRL
• HOL
• ETPS
• HOL Light
• Nuprl
• NQTHM
• IMPS
• MetaOCaml
• Agda
• MathScheme
• Idris
• reFLect
• HOL Light QE
• MiniML

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

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