Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
From MaRDI portal
Publication:438569
DOI10.1007/S10817-010-9194-XzbMATH Open1252.68252OpenAlexW2140849218MaRDI QIDQ438569FDOQ438569
Amy P. Felty, Alberto Momigliano
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
Recommendations
- Two-level hybrid: a system for reasoning using higher-order abstract syntax
- A Hybrid Denotational Semantics for Hybrid Systems
- Higher-order syntax and saturation algorithms for hybrid logic
- A Hybrid Intuitionistic Logic: Semantics and Decidability
- Hybrid logic and its proof-theory
- Constructive description logics hybrid-style
- Reasoning with higher-order abstract syntax in a logical framework
- Foundations of Software Science and Computation Structures
- Denotational semantics of hybrid automata
- Foundations of Logic Programming in Hybridised Logics
inductionCoqhigher-order abstract syntaxinteractive theorem provingIsabelle/HOLlogical frameworksvariable binding
Cites Work
- The Twelf Proof Assistant
- Ott
- The Abella Interactive Theorem Prover (System Description)
- Theorem Proving in Higher Order Logics
- Isabelle/HOL. A proof assistant for higher-order logic
- Nominal logic, a first order theory of names and binding
- Some lambda calculus and type theory formalized
- Alpha-structural recursion and induction
- A framework for defining logics
- Title not available (Why is that?)
- A new approach to abstract syntax with variable binding
- Logic programming in a fragment of intuitionistic linear logic
- Proving congruence of bisimulation in functional programming languages
- Types for Proofs and Programs
- 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 Coverage Checking Algorithm for LF
- Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Types for Proofs and Programs
- Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison
- Verifying termination and reduction properties about higher-order logic programs
- Title not available (Why is that?)
- Partial inductive definitions
- Title not available (Why is that?)
- Uniform proofs as a foundation for logic programming
- Towards a mechanized metatheory of standard ML
- Title not available (Why is that?)
- The representational adequacy of <scp>Hybrid</scp>
- Engineering formal metatheory
- Full abstraction in the lazy lambda calculus
- 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
- On the formalization of the modal \(\mu\)-calculus in the calculus of inductive constructions
- Executable JVM model for analytical reasoning: A study
- Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts
- Title not available (Why is that?)
- Title not available (Why is that?)
- A meta linear logical framework
- Title not available (Why is that?)
- A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL
- Higher-order abstract syntax in type theory
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- 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
- 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
- Automated Deduction – CADE-19
- Primitive recursion for higher-order abstract syntax
- Forum: A multiple-conclusion specification logic
Cited In (26)
- A case study in programming coinductive proofs: Howe’s method
- Rensets and renaming-based recursion for syntax with bindings
- A focused linear logical framework and its application to metatheory of object logics
- Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions
- Formalization of metatheory of the Quipper quantum programming language in a linear logic
- Formal meta-level analysis framework for quantum programming languages
- Mechanized metatheory revisited
- Canonical HybridLF: extending Hybrid with dependent types
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Programs Using Syntax with First-Class Binders
- A formalized general theory of syntax with bindings
- The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
- A formalized general theory of syntax with bindings: extended version
- POPLMark reloaded: Mechanizing proofs by logical relations
- Mechanizing proofs with logical relations – Kripke-style
- Title not available (Why is that?)
- Mechanizing focused linear logic in Coq
- Higher-order abstract syntax in type theory
- Cut elimination for a logic with induction and co-induction
- A two-level logic approach to reasoning about computations
- Towards substructural property-based testing
- Rensets and renaming-based recursion for syntax with bindings extended version
- Term-generic logic
- Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq
Uses Software
This page was built for publication: Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q438569)
