Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
From MaRDI portal
Publication:438569
DOI10.1007/s10817-010-9194-xzbMath1252.68252OpenAlexW2140849218MaRDI QIDQ438569
Alberto Momigliano, Amy P. Felty
Publication date: 31 July 2012
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-010-9194-x
inductionhigher-order abstract syntaxIsabelle/HOLinteractive theorem provinglogical frameworksCoqvariable binding
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (21)
The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey ⋮ A two-level logic approach to reasoning about computations ⋮ A formalized general theory of syntax with bindings ⋮ Towards substructural property-based testing ⋮ Rensets and renaming-based recursion for syntax with bindings extended version ⋮ POPLMark reloaded: Mechanizing proofs by logical relations ⋮ Cut elimination for a logic with induction and co-induction ⋮ Programs Using Syntax with First-Class Binders ⋮ A formalized general theory of syntax with bindings: extended version ⋮ Canonical HybridLF: extending Hybrid with dependent types ⋮ Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions ⋮ Mechanizing proofs with logical relations – Kripke-style ⋮ Unnamed Item ⋮ A case study in programming coinductive proofs: Howe’s method ⋮ Mechanized metatheory revisited ⋮ Formalization of metatheory of the Quipper quantum programming language in a linear logic ⋮ Formal meta-level analysis framework for quantum programming languages ⋮ Mechanizing focused linear logic in Coq ⋮ Term-generic logic ⋮ Rensets and renaming-based recursion for syntax with bindings ⋮ A focused linear logical framework and its application to metatheory of object logics
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
- Unnamed Item
- Forum: A multiple-conclusion specification logic
- A new approach to abstract syntax with variable binding
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Verifying termination and reduction properties about higher-order logic programs
- Partial inductive definitions
- Full abstraction in the lazy lambda calculus
- Logic programming in a fragment of intuitionistic linear logic
- A linear logical framework
- A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names.
- Formal foundations of operational semantics
- Cut-elimination for a logic with definitions and induction
- Isabelle/HOL. A proof assistant for higher-order logic
- On the formalization of the modal \(\mu\)-calculus in the calculus of inductive constructions
- Nominal logic, a first order theory of names and binding
- Proving congruence of bisimulation in functional programming languages
- Some lambda calculus and type theory formalized
- Executable JVM model for analytical reasoning: A study
- Uniform proofs as a foundation for logic programming
- Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts
- A Meta Linear Logical Framework
- The representational adequacy of <scp>Hybrid</scp>
- The Twelf Proof Assistant
- Towards a mechanized metatheory of standard ML
- Engineering formal metatheory
- The Abella Interactive Theorem Prover (System Description)
- Alpha-structural recursion and induction
- A Coverage Checking Algorithm for LF
- Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq
- A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL
- A framework for defining logics
- Ott
- Parametric higher-order abstract syntax for mechanized semantics
- Automated Deduction – CADE-20
- Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism
- Practical Programming with Higher-Order Encodings and Dependent Types
- Theorem Proving in Higher Order Logics
- Consistency of the theory of contexts
- Theorem Proving in Higher Order Logics
- Linearity Constraints as Bounded Intervals in Linear Logic Programming
- Frontiers of Combining Systems
- Mechanized meta-reasoning using a hybrid HOAS/de bruijn representation and reflection
- Typed Lambda Calculi and Applications
- Foundations of Software Science and Computational Structures
- Types for Proofs and Programs
- Types for Proofs and Programs
- Types for Proofs and Programs
- Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison
- A formulation of the simple theory of types
- Automated Deduction – CADE-19
- Primitive recursion for higher-order abstract syntax
This page was built for publication: Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
