A two-level logic approach to reasoning about computations

DOI10.1007/S10817-011-9218-1zbMATH Open1290.68088arXiv0911.2993OpenAlexW1678615379MaRDI QIDQ2392484FDOQ2392484

Authors: Andrew Gacek, Gopalan Nadathur, Dale Miller 

Publication date: 1 August 2013

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

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.

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

Recommendations

• A two-level logic approach to reasoning about typed specification languages
• Abella: a system for reasoning about relational specifications
• The Abella Interactive Theorem Prover (System Description)
• Nominal abstraction
• Reasoning in Abella about structural operational semantics specifications

zbMATH Keywords

generic judgments\(\lambda\)-tree syntax\(\nabla\)-quantificationnominal abstractiontwo-level logic

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Combinatory logic and lambda calculus (03B40) Functional programming and lambda calculus (68N18)

Cites Work

• The Abella Interactive Theorem Prover (System Description)
• Theorem Proving in Higher Order Logics
• Nominal techniques in Isabelle/HOL
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• LCF considered as a programming language
• Isabelle/HOL. A proof assistant for higher-order logic
• Nominal logic, a first order theory of names and binding
• Functions as processes
• A framework for defining logics
• A formulation of the simple theory of types
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
• Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
• Nominal abstraction
• Unification under a mixed prefix
• Title not available (Why is that?)
• Uniform proofs as a foundation for logic programming
• The Mechanical Evaluation of Expressions
• Title not available (Why is that?)
• Engineering formal metatheory
• Cut-elimination for a logic with definitions and induction
• Title not available (Why is that?)
• Types for Proofs and Programs
• Title not available (Why is that?)
• The lazy lambda calculus in a concurrency scenario
• A logic for reasoning about generic judgments

Cited In (25)

• Proving concurrent constraint programming correct, revisited
• Subformula linking for intuitionistic logic with application to type theory
• Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions
• Logical Difference Computation with CEX2.5
• Mechanized metatheory revisited
• Formalized meta-theory of sequent calculi for substructural logics
• Programs Using Syntax with First-Class Binders
• Proof checking and logic programming
• The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
• Nominal abstraction
• LINCX: A Linear Logical Framework with First-Class Contexts
• Formalized meta-theory of sequent calculi for linear logics
• Title not available (Why is that?)
• Proof pearl: Abella formalization of \(\lambda \)-calculus cube property
• Cut elimination for a logic with induction and co-induction
• αCheck: A mechanized metatheory model checker
• Divergence and unique solution of equations
• Title not available (Why is that?)
• Towards substructural property-based testing
• Connecting logical representations and efficient computations
• Proof Checking and Logic Programming
• A proof theory for model checking
• Term-generic logic
• Towards two-level formal modeling of computer-based systems
• A Survey of the Proof-Theoretic Foundations of Logic Programming

Uses Software

• Coq
• HYBRID
• Isabelle/HOL
• Twelf
• Bedwyr
• Abella
• PoplMark
• Nominal Isabelle
• Teyjus
• Delphin

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)