Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax

DOI10.1007/S10817-010-9194-XMaRDI QIDQ438569zbMATH OpenOpenAlexFDO

Authors 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

zbMATH Keywords

inductionCoqhigher-order abstract syntaxinteractive theorem provingIsabelle/HOLlogical frameworksvariable binding

Mathematics Subject Classification ID

Logic in computer science (03B70)

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

Cites work

• scientific article; zbMATH DE number 1614713 (Why is no real title available?)
• scientific article; zbMATH DE number 1670734 (Why is no real title available?)
• scientific article; zbMATH DE number 1692891 (Why is no real title available?)
• scientific article; zbMATH DE number 2185657 (Why is no real title available?)
• scientific article; zbMATH DE number 65527 (Why is no real title available?)
• scientific article; zbMATH DE number 1330453 (Why is no real title available?)
• scientific article; zbMATH DE number 512790 (Why is no real title available?)
• scientific article; zbMATH DE number 1078585 (Why is no real title available?)
• scientific article; zbMATH DE number 1158759 (Why is no real title available?)
• scientific article; zbMATH DE number 1956525 (Why is no real title available?)
• scientific article; zbMATH DE number 1927412 (Why is no real title available?)
• scientific article; zbMATH DE number 1927423 (Why is no real title available?)
• scientific article; zbMATH DE number 1497779 (Why is no real title available?)
• scientific article; zbMATH DE number 1508934 (Why is no real title available?)
• scientific article; zbMATH DE number 1754648 (Why is no real title available?)
• scientific article; zbMATH DE number 2134912 (Why is no real title available?)
• A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL
• A coverage checking algorithm for LF
• A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names.
• A formulation of the simple theory of types
• A framework for defining logics
• A linear logical framework
• A meta linear logical framework
• A new approach to abstract syntax with variable binding
• Alpha-structural recursion and induction
• Automated Deduction – CADE-19
• Automated Deduction – CADE-20
• Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism
• Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq
• Consistency of the theory of contexts
• Cut-elimination for a logic with definitions and induction
• Engineering formal metatheory
• Executable JVM model for analytical reasoning: A study
• Formal foundations of operational semantics
• Forum: A multiple-conclusion specification logic
• Foundations of Software Science and Computational Structures
• Frontiers of Combining Systems
• Full abstraction in the lazy lambda calculus
• Higher-order abstract syntax in type theory
• 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
• Linearity Constraints as Bounded Intervals in Linear Logic Programming
• Logic programming in a fragment of intuitionistic linear logic
• Mechanized meta-reasoning using a hybrid HOAS/de Bruijn representation and reflection
• Nominal logic, a first order theory of names and binding
• On the formalization of the modal -calculus in the calculus of inductive constructions
• Ott, effective tool support for the working semanticist
• Parametric higher-order abstract syntax for mechanized semantics
• Partial inductive definitions
• Practical Programming with Higher-Order Encodings and Dependent Types
• Primitive recursion for higher-order abstract syntax
• Proving congruence of bisimulation in functional programming languages
• Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts
• Reasoning with higher-order abstract syntax and contexts: a comparison
• Some lambda calculus and type theory formalized
• The Abella Interactive Theorem Prover (System Description)
• The Twelf Proof Assistant
• The representational adequacy of Hybrid
• Theorem Proving in Higher Order Logics
• Theorem Proving in Higher Order Logics
• Towards a mechanized metatheory of Standard ML
• Typed Lambda Calculi and Applications
• Types for Proofs and Programs
• Types for Proofs and Programs
• Types for Proofs and Programs
• Uniform proofs as a foundation for logic programming
• Verifying termination and reduction properties about higher-order logic programs

Cited in

(30)

• Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq
• Programs using syntax with first-class binders
• Rensets and renaming-based recursion for syntax with bindings
• A focused linear logical framework and its application to metatheory of object logics
• Formalization of metatheory of the Quipper quantum programming language in a linear logic
• Formal meta-level analysis framework for quantum programming languages
• Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions
• Canonical HybridLF: extending Hybrid with dependent types
• Mechanized metatheory revisited
• scientific article; zbMATH DE number 2185657 (Why is no real title available?)
• A formalized general theory of syntax with bindings
• The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
• scientific article; zbMATH DE number 1927412 (Why is no real title available?)
• scientific article; zbMATH DE number 1956525 (Why is no real title available?)
• A formalized general theory of syntax with bindings: extended version
• A case study in programming coinductive proofs: Howe's method
• The representational adequacy of Hybrid
• scientific article; zbMATH DE number 7204440 (Why is no real title available?)
• Mechanizing focused linear logic in Coq
• Higher-order abstract syntax in type theory
• Reasoning with higher-order abstract syntax and contexts: a comparison
• Cut elimination for a logic with induction and co-induction
• A two-level logic approach to reasoning about computations
• POPLMark reloaded: mechanizing proofs by logical relations
• Towards substructural property-based testing
• A hybrid encoding of Howe's method for establishing congruence of bisimilarity
• Rensets and renaming-based recursion for syntax with bindings extended version
• Two-level hybrid: a system for reasoning using higher-order abstract syntax
• Mechanizing proofs with logical relations -- Kripke-style
• Term-generic logic

Describes a project that uses

Uses Software

• Lolli
• mini-ML
• Nominal Isabelle
• PoplMark
• LEGO
• Abella
• Bedwyr
• Twelf
• Isabelle/ZF
• Isar
• PVS
• Isabelle/HOL
• Ott
• Isabelle
• HYBRID
• Coq

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)