Incorporating quotation and evaluation into Church's type theory
From MaRDI portal
Publication:1753993
DOI10.1016/j.ic.2018.03.001zbMath1390.68168arXiv1612.02785OpenAlexW2581306138MaRDI QIDQ1753993
Publication date: 30 May 2018
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1612.02785
reflectionevaluationsymbolic computationschemasmetareasoningsubstitutionsimple type theoryquotationChurch's type theorymeaning formulasquasiquotationreasoning about syntax
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A new approach to abstract syntax with variable binding
- Directly reflective meta-programming
- \textit{Theorema}: Towards computer-aided mathematical theory exploration
- Proof synthesis and reflection for linear arithmetic
- The seven virtues of simple type theory
- Automatic synthesis of typed \(\Lambda\)-programs on term algebras
- The calculus of constructions
- A simple type theory with partial functions and subtypes
- IMPS: An interactive mathematical proof system
- MetaML and multi-stage programming with explicit annotations
- Reflection in conditional rewriting logic
- HOL Light QE
- An introduction to mathematical logic and type theory: To truth through proof.
- Nominal logic, a first order theory of names and binding
- 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: 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
- Axiomatizing the Quote
- Elaborator reflection: extending Idris in Idris
- Andrews' Type Theory with Undefinedness
- Tactics for Reasoning Modulo AC in Coq
- HOL Light: An Overview
- A modal analysis of staged computation
- A reflective functional language for hardware design and theorem proving
- Generic Literals
- Certification of Automated Termination Proofs
- The Four Colour Theorem: Engineering of a Formal Proof
- Syntax for Free: Representing Syntax with Binding Using Parametricity
- Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages
- Dependently Typed Programming in Agda
- The Impact of the Lambda Calculus in Logic and Computer Science
- IMPS: An updated system description
- Explicit substitutions
- Typed self-interpretation by pattern matching
- MathScheme: Project Description
- Contextual modal type theory
- Automated Reasoning
- A Machine-Checked Proof of the Odd Order Theorem
- Typed self-evaluation via intensional type functions
- Biform Theories in Chiron
- Theorem Proving in Higher Order Logics
- Theorem Proving in Higher Order Logics
- Meta Reasoning in ACL2
- High-Level Theories
- Staged computation with names and necessity
- A partial functions version of Church's simple theory of types
- Completeness in the theory of types
- On reflection principles
- Proof by computation in the Coq system
