A two-level logic approach to reasoning about computations
From MaRDI portal
Publication:2392484
Abstract: Relational descriptions have been used in formalizing diverse computational notions, including, for example, operational semantics, typing, and acceptance by non-deterministic machines. We therefore propose a (restricted) logical theory over relations as a language for specifying such notions. Our specification logic is further characterized by an ability to explicitly treat binding in object languages. Once such a logic is fixed, a natural next question is how we might prove theorems about specifications written in it. We propose to use a second logic, called a reasoning logic, for this purpose. A satisfactory reasoning logic should be able to completely encode the specification logic. Associated with the specification logic are various notions of binding: for quantifiers within formulas, for eigenvariables within sequents, and for abstractions within terms. To provide a natural treatment of these aspects, the reasoning logic must encode binding structures as well as their associated notions of scope, free and bound variables, and capture-avoiding substitution. Further, to support arguments about provability, the reasoning logic should possess strong mechanisms for constructing proofs by induction and co-induction. We provide these capabilities here by using a logic called G which represents relations over lambda-terms via definitions of atomic judgments, contains inference rules for induction and co-induction, and includes a special generic quantifier. We show how provability in the specification logic can be transparently encoded in G. We also describe an interactive theorem prover called Abella that implements G and this two-level logic approach and we present several examples that demonstrate the efficacy of Abella in reasoning about computations.
Recommendations
Cites work
- scientific article; zbMATH DE number 1696799 (Why is no real title available?)
- scientific article; zbMATH DE number 2185657 (Why is no real title available?)
- scientific article; zbMATH DE number 4035108 (Why is no real title available?)
- scientific article; zbMATH DE number 4189687 (Why is no real title available?)
- A formulation of the simple theory of types
- A framework for defining logics
- A logic for reasoning about generic judgments
- A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
- Call-by-name, call-by-value and the \(\lambda\)-calculus
- Cut-elimination for a logic with definitions and induction
- Engineering formal metatheory
- Functions as processes
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Isabelle/HOL. A proof assistant for higher-order logic
- LCF considered as a programming language
- Nominal abstraction
- Nominal logic, a first order theory of names and binding
- Nominal techniques in Isabelle/HOL
- The Abella Interactive Theorem Prover (System Description)
- The Mechanical Evaluation of Expressions
- The lazy lambda calculus in a concurrency scenario
- Theorem Proving in Higher Order Logics
- Types for Proofs and Programs
- Unification under a mixed prefix
- Uniform proofs as a foundation for logic programming
Cited in
(28)- The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
- \textsc{Lincx}: a linear logical framework with first-class contexts
- Proof checking and logic programming
- scientific article; zbMATH DE number 7204440 (Why is no real title available?)
- Proof checking and logic programming
- Formalized meta-theory of sequent calculi for linear logics
- Cut elimination for a logic with induction and co-induction
- Logical Difference Computation with CEX2.5
- Towards two-level formal modeling of computer-based systems
- Proof pearl: Abella formalization of \(\lambda \)-calculus cube property
- Towards substructural property-based testing
- Nominal abstraction
- A proof theory for model checking
- Programs using syntax with first-class binders
- αCheck: A mechanized metatheory model checker
- Term-generic logic
- A Survey of the Proof-Theoretic Foundations of Logic Programming
- A characterisation of open bisimilarity using an intuitionistic modal logic
- Mechanized metatheory revisited
- Formalized meta-theory of sequent calculi for substructural logics
- Connecting logical representations and efficient computations
- A two-level logic approach to reasoning about typed specification languages
- Subformula linking for intuitionistic logic with application to type theory
- Reasoning in Abella about structural operational semantics specifications
- Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions
- Proving concurrent constraint programming correct, revisited
- Abella: a system for reasoning about relational specifications
- scientific article; zbMATH DE number 7407774 (Why is no real title available?)
Describes a project that uses
Uses Software
This page was built for publication: A two-level logic approach to reasoning about computations
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2392484)
