Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (Q438569): Difference between revisions

@@ Property / describes a project that uses @@
+PoplMark
@@ Property / describes a project that uses: PoplMark / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Nominal Isabelle
@@ Property / describes a project that uses: Nominal Isabelle / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle
@@ Property / describes a project that uses: Isabelle / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Bedwyr
@@ Property / describes a project that uses: Bedwyr / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+mini-ML
@@ Property / describes a project that uses: mini-ML / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Lolli
@@ Property / describes a project that uses: Lolli / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Coq
@@ Property / describes a project that uses: Coq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle/HOL
@@ Property / describes a project that uses: Isabelle/HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isar
@@ Property / describes a project that uses: Isar / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle/ZF
@@ Property / describes a project that uses: Isabelle/ZF / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Twelf
@@ Property / describes a project that uses: Twelf / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/s10817-010-9194-x
+Normal rank
@@ Property / OpenAlex ID @@
+W2140849218
@@ Property / OpenAlex ID: W2140849218 / rank @@
+Normal rank
@@ Property / cites work @@
+Full abstraction in the lazy lambda calculus
@@ Property / cites work: Full abstraction in the lazy lambda calculus / rank @@
+Normal rank
@@ Property / cites work @@
+Q4484329
@@ Property / cites work: Q4484329 / rank @@
+Normal rank
@@ Property / cites work @@
+Engineering formal metatheory
@@ Property / cites work: Engineering formal metatheory / rank @@
+Normal rank
@@ Property / cites work @@
+Theorem Proving in Higher Order Logics
@@ Property / cites work: Theorem Proving in Higher Order Logics / rank @@
+Normal rank
@@ Property / cites work @@
+Types for Proofs and Programs
@@ Property / cites work: Types for Proofs and Programs / rank @@
+Normal rank
@@ Property / cites work @@
+Q2754030
@@ Property / cites work: Q2754030 / rank @@
+Normal rank
@@ Property / cites work @@
+Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
+Normal rank
@@ Property / cites work @@
+Consistency of the theory of contexts
@@ Property / cites work: Consistency of the theory of contexts / rank @@
+Normal rank
@@ Property / cites work @@
+Q3656423
@@ Property / cites work: Q3656423 / rank @@
+Normal rank
@@ Property / cites work @@
+Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq
+Normal rank
@@ Property / cites work @@
+A linear logical framework
@@ Property / cites work: A linear logical framework / rank @@
+Normal rank
@@ Property / cites work @@
+Foundations of Software Science and Computational Structures
+Normal rank
@@ Property / cites work @@
+Parametric higher-order abstract syntax for mechanized semantics
+Normal rank
@@ Property / cites work @@
+A formulation of the simple theory of types
@@ Property / cites work: A formulation of the simple theory of types / rank @@
+Normal rank
@@ Property / cites work @@
+Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts
+Normal rank
@@ Property / cites work @@
+Automated Deduction – CADE-19
@@ Property / cites work: Automated Deduction – CADE-19 / rank @@
+Normal rank
@@ Property / cites work @@
+The representational adequacy of <scp>Hybrid</scp>
+Normal rank
@@ Property / cites work @@
+Frontiers of Combining Systems
@@ Property / cites work: Frontiers of Combining Systems / rank @@
+Normal rank
@@ Property / cites work @@
+Q4499196
@@ Property / cites work: Q4499196 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4012875
@@ Property / cites work: Q4012875 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3024831
@@ Property / cites work: Q3024831 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4506397
@@ Property / cites work: Q4506397 / rank @@
+Normal rank
@@ Property / cites work @@
+Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison
+Normal rank
@@ Property / cites work @@
+Q4484341
@@ Property / cites work: Q4484341 / rank @@
+Normal rank
@@ Property / cites work @@
+Formal foundations of operational semantics
@@ Property / cites work: Formal foundations of operational semantics / rank @@
+Normal rank
@@ Property / cites work @@
+A new approach to abstract syntax with variable binding
+Normal rank
@@ Property / cites work @@
+The Abella Interactive Theorem Prover (System Description)
+Normal rank
@@ Property / cites work @@
+Q2723440
@@ Property / cites work: Q2723440 / rank @@
+Normal rank
@@ Property / cites work @@
+Partial inductive definitions
@@ Property / cites work: Partial inductive definitions / rank @@
+Normal rank
@@ Property / cites work @@
+A framework for defining logics
@@ Property / cites work: A framework for defining logics / rank @@
+Normal rank
@@ Property / cites work @@
+Mechanized meta-reasoning using a hybrid HOAS/de bruijn representation and reflection
+Normal rank
@@ Property / cites work @@
+Q4391450
@@ Property / cites work: Q4391450 / rank @@
+Normal rank
@@ Property / cites work @@
+Logic programming in a fragment of intuitionistic linear logic
+Normal rank
@@ Property / cites work @@
+Q4535076
@@ Property / cites work: Q4535076 / rank @@
+Normal rank
@@ Property / cites work @@
+Proving congruence of bisimulation in functional programming languages
+Normal rank
@@ Property / cites work @@
+Towards a mechanized metatheory of standard ML
@@ Property / cites work: Towards a mechanized metatheory of standard ML / rank @@
+Normal rank
@@ Property / cites work @@
+Executable JVM model for analytical reasoning: A study
+Normal rank
@@ Property / cites work @@
+Q4360856
@@ Property / cites work: Q4360856 / rank @@
+Normal rank
@@ Property / cites work @@
+A Meta Linear Logical Framework
@@ Property / cites work: A Meta Linear Logical Framework / rank @@
+Normal rank
@@ Property / cites work @@
+Cut-elimination for a logic with definitions and induction
+Normal rank
@@ Property / cites work @@
+Some lambda calculus and type theory formalized
@@ Property / cites work: Some lambda calculus and type theory formalized / rank @@
+Normal rank
@@ Property / cites work @@
+On the formalization of the modal \(\mu\)-calculus in the calculus of inductive constructions
+Normal rank
@@ Property / cites work @@
+Forum: A multiple-conclusion specification logic
@@ Property / cites work: Forum: A multiple-conclusion specification logic / rank @@
+Normal rank
@@ Property / cites work @@
+Q4650578
@@ Property / cites work: Q4650578 / rank @@
+Normal rank
@@ Property / cites work @@
+Uniform proofs as a foundation for logic programming
+Normal rank
@@ Property / cites work @@
+Q4417871
@@ Property / cites work: Q4417871 / rank @@
+Normal rank
@@ Property / cites work @@
+Types for Proofs and Programs
@@ Property / cites work: Types for Proofs and Programs / rank @@
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+Theorem Proving in Higher Order Logics
@@ Property / cites work: Theorem Proving in Higher Order Logics / rank @@
+Normal rank
@@ Property / cites work @@
+Q4281483
@@ Property / cites work: Q4281483 / rank @@
+Normal rank
@@ Property / cites work @@
+Verifying termination and reduction properties about higher-order logic programs
+Normal rank
@@ Property / cites work @@
+Nominal logic, a first order theory of names and binding
+Normal rank
@@ Property / cites work @@
+Alpha-structural recursion and induction
@@ Property / cites work: Alpha-structural recursion and induction / rank @@
+Normal rank
@@ Property / cites work @@
+Q2763630
@@ Property / cites work: Q2763630 / rank @@
+Normal rank
@@ Property / cites work @@
+Linearity Constraints as Bounded Intervals in Linear Logic Programming
+Normal rank
@@ Property / cites work @@
+Q4261096
@@ Property / cites work: Q4261096 / rank @@
+Normal rank
@@ Property / cites work @@
+Practical Programming with Higher-Order Encodings and Dependent Types
+Normal rank
@@ Property / cites work @@
+The Twelf Proof Assistant
@@ Property / cites work: The Twelf Proof Assistant / rank @@
+Normal rank
@@ Property / cites work @@
+Primitive recursion for higher-order abstract syntax
+Normal rank
@@ Property / cites work @@
+A Coverage Checking Algorithm for LF
@@ Property / cites work: A Coverage Checking Algorithm for LF / rank @@
+Normal rank
@@ Property / cites work @@
+Typed Lambda Calculi and Applications
@@ Property / cites work: Typed Lambda Calculi and Applications / rank @@
+Normal rank
@@ Property / cites work @@
+Ott
@@ Property / cites work: Ott / rank @@
+Normal rank
@@ Property / cites work @@
+A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+Automated Deduction – CADE-20
@@ Property / cites work: Automated Deduction – CADE-20 / rank @@
+Normal rank
@@ Property / cites work @@
+A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names.
+Normal rank
@@ Property / cites work @@
+Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism
+Normal rank
@@ Property / cites work @@
+Types for Proofs and Programs
@@ Property / cites work: Types for Proofs and Programs / rank @@
+Normal rank