Incorporating Quotation and Evaluation into Church’s Type Theory: Syntax and Semantics

DOI10.1007/978-3-319-42547-4_7zbMath1344.68204arXiv1605.07068OpenAlexW2962936422MaRDI QIDQ2817296

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)

Related Items (3)

Theory morphisms in Church's type theory with quotation and evaluation ⋮ Formalizing mathematical knowledge as a biform theory graph: a case study ⋮ Incorporating quotation and evaluation into Church's type theory

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Directly reflective meta-programming
• MetaML and multi-stage programming with explicit annotations
• An introduction to mathematical logic and type theory: To truth through proof.
• The Formalization of Syntax-Based Mathematical Algorithms Using Quotation and Evaluation
• HOL Light: An Overview
• A reflective functional language for hardware design and theorem proving
• Dependently Typed Programming in Agda
• Explicit substitutions
• A formulation of the simple theory of types
• Completeness in the theory of types

This page was built for publication: Incorporating Quotation and Evaluation into Church’s Type Theory: Syntax and Semantics