Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
type: Item
instance of: scholarly article
title: Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
zbMATH Open document ID: 1252.68252
author: Alberto Momigliano
author: Amy P. Felty
published in: Journal of Automated Reasoning
publication date: 2012-07-31T00:00:00Z
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 03B70
zbMATH DE Number: 6062061
zbMATH Keywords: logical frameworks
zbMATH Keywords: higher-order abstract syntax
zbMATH Keywords: interactive theorem proving
zbMATH Keywords: induction
zbMATH Keywords: variable binding
zbMATH Keywords: Isabelle/HOL
zbMATH Keywords: Coq
describes a project that uses: HYBRID
describes a project that uses: Ott
describes a project that uses: PVS
describes a project that uses: Abella
describes a project that uses: LEGO
describes a project that uses: PoplMark
describes a project that uses: Nominal Isabelle
describes a project that uses: Isabelle
describes a project that uses: Bedwyr
describes a project that uses: mini-ML
describes a project that uses: Lolli
describes a project that uses: Coq
describes a project that uses: Isabelle/HOL
describes a project that uses: Isar
describes a project that uses: Isabelle/ZF
describes a project that uses: Twelf
MaRDI profile type: Publication
full work available at URL: s10817-010-9194-x
OpenAlex ID: W2140849218
cites work: Full abstraction in the lazy lambda calculus
cites work: Q4484329
cites work: Engineering formal metatheory
cites work: Theorem Proving in Higher Order Logics
cites work: Types for Proofs and Programs
cites work: Q2754030
cites work: Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
cites work: Consistency of the theory of contexts
cites work: Q3656423
cites work: Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq
cites work: A linear logical framework
cites work: Foundations of Software Science and Computational Structures
cites work: Parametric higher-order abstract syntax for mechanized semantics
cites work: A formulation of the simple theory of types
cites work: Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts
cites work: Automated Deduction – CADE-19
cites work: The representational adequacy of <scp>Hybrid</scp>
cites work: Frontiers of Combining Systems
cites work: Q4499196
cites work: Q4012875
cites work: Q3024831
cites work: Q4506397
cites work: Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison
cites work: Q4484341
cites work: Formal foundations of operational semantics
cites work: A new approach to abstract syntax with variable binding
cites work: The Abella Interactive Theorem Prover (System Description)
cites work: Q2723440
cites work: Partial inductive definitions
cites work: A framework for defining logics
cites work: Mechanized meta-reasoning using a hybrid HOAS/de bruijn representation and reflection
cites work: Q4391450
cites work: Logic programming in a fragment of intuitionistic linear logic
cites work: Q4535076
cites work: Proving congruence of bisimulation in functional programming languages
cites work: Towards a mechanized metatheory of standard ML
cites work: Executable JVM model for analytical reasoning: A study
cites work: Q4360856
cites work: A meta linear logical framework
cites work: Cut-elimination for a logic with definitions and induction
cites work: Some lambda calculus and type theory formalized
cites work: On the formalization of the modal \(\mu\)-calculus in the calculus of inductive constructions
cites work: Forum: A multiple-conclusion specification logic

Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (cites work)
cites work: Q4650578

Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (cites work)
cites work: Uniform proofs as a foundation for logic programming

Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (cites work)
cites work: Q4417871

Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (cites work)
cites work: Types for Proofs and Programs

Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (cites work)
cites work: Isabelle/HOL. A proof assistant for higher-order logic

Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (cites work)
cites work: Theorem Proving in Higher Order Logics

Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (cites work)
cites work: Q4281483

Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (cites work)
cites work: Verifying termination and reduction properties about higher-order logic programs

Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (cites work)
cites work: Nominal logic, a first order theory of names and binding

Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (cites work)
cites work: Alpha-structural recursion and induction

Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (cites work)
cites work: Q2763630

Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (cites work)
cites work: Linearity Constraints as Bounded Intervals in Linear Logic Programming

Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (cites work)
cites work: Q4261096

Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (cites work)
cites work: Practical Programming with Higher-Order Encodings and Dependent Types

Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (cites work)
cites work: The Twelf Proof Assistant

Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (cites work)
cites work: Primitive recursion for higher-order abstract syntax

Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (cites work)
cites work: A Coverage Checking Algorithm for LF

Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (cites work)
cites work: Typed Lambda Calculi and Applications

Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (cites work)
cites work: Ott

Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (cites work)
cites work: A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL

Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (cites work)
cites work: Automated Deduction – CADE-20

Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (cites work)
cites work: A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names.

Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (cites work)
cites work: Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism

Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (cites work)
cites work: Types for Proofs and Programs

Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (DOI)
DOI: 10.1007/S10817-010-9194-X

Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (Recommended article)
Recommended article: Two-level hybrid: a system for reasoning using higher-order abstract syntax
Similarity Score: 0.944105
Recommender Run: Recommender Run 3

Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (Recommended article)
Recommended article: A Hybrid Denotational Semantics for Hybrid Systems
Similarity Score: 0.8815013
Recommender Run: Recommender Run 3

Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (Recommended article)
Recommended article: Higher-order syntax and saturation algorithms for hybrid logic
Similarity Score: 0.87376064
Recommender Run: Recommender Run 3

Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (Recommended article)
Recommended article: A Hybrid Intuitionistic Logic: Semantics and Decidability
Similarity Score: 0.8623357
Recommender Run: Recommender Run 3

Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (Recommended article)
Recommended article: Hybrid logic and its proof-theory
Similarity Score: 0.86054355
Recommender Run: Recommender Run 3

Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (Recommended article)
Recommended article: Constructive Description Logics Hybrid-Style
Similarity Score: 0.85986376
Recommender Run: Recommender Run 3

Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (Recommended article)
Recommended article: Reasoning with higher-order abstract syntax in a logical framework
Similarity Score: 0.85976917
Recommender Run: Recommender Run 3

Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (Recommended article)
Recommended article: Foundations of Software Science and Computation Structures
Similarity Score: 0.8553032
Recommender Run: Recommender Run 3

Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (Recommended article)
Recommended article: Denotational semantics of hybrid automata
Similarity Score: 0.8553032
Recommender Run: Recommender Run 3

Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (Recommended article)
Recommended article: Foundations of Logic Programming in Hybridised Logics
Similarity Score: 0.8533792
Recommender Run: Recommender Run 3