A formalized general theory of syntax with bindings: extended version (Q1984791): Difference between revisions

@@ Property / describes a project that uses @@
+HOL
@@ Property / describes a project that uses: HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HoTT
@@ Property / describes a project that uses: HoTT / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+AmiCo
@@ Property / describes a project that uses: AmiCo / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HYBRID
@@ Property / describes a project that uses: HYBRID / 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 @@
+Ott
@@ Property / describes a project that uses: Ott / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Psi-calculi
@@ Property / describes a project that uses: Psi-calculi / 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 @@
+Twelf
@@ Property / describes a project that uses: Twelf / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Abella
@@ Property / describes a project that uses: Abella / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Gmeta
@@ Property / describes a project that uses: Gmeta / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+LNgen
@@ Property / describes a project that uses: LNgen / 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 @@
+Locales
@@ Property / describes a project that uses: Locales / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Delphin
@@ Property / describes a project that uses: Delphin / 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-019-09522-2
+Normal rank
@@ Property / OpenAlex ID @@
+W2935704972
@@ Property / OpenAlex ID: W2935704972 / rank @@
+Normal rank
@@ Property / cites work @@
+A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
+Normal rank
@@ Property / cites work @@
+Indexed containers
@@ Property / cites work: Indexed containers / rank @@
+Normal rank
@@ Property / cites work @@
+Q4945244
@@ Property / cites work: Q4945244 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2871861
@@ Property / cites work: Q2871861 / rank @@
+Normal rank
@@ Property / cites work @@
+Engineering formal metatheory
@@ Property / cites work: Engineering formal metatheory / rank @@
+Normal rank
@@ Property / cites work @@
+Abella: A System for Reasoning about Relational Specifications
+Normal rank
@@ Property / cites work @@
+Psi-calculi in Isabelle
@@ Property / cites work: Psi-calculi in Isabelle / rank @@
+Normal rank
@@ Property / cites work @@
+Q2871859
@@ Property / cites work: Q2871859 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4945200
@@ Property / cites work: Q4945200 / rank @@
+Normal rank
@@ Property / cites work @@
+de Bruijn notation as a nested datatype
@@ Property / cites work: de Bruijn notation as a nested datatype / rank @@
+Normal rank
@@ Property / cites work @@
+Encoding Monomorphic and Polymorphic Types
@@ Property / cites work: Encoding Monomorphic and Polymorphic Types / rank @@
+Normal rank
@@ Property / cites work @@
+Friends with Benefits
@@ Property / cites work: Friends with Benefits / rank @@
+Normal rank
@@ Property / cites work @@
+Truly Modular (Co)datatypes for Isabelle/HOL
@@ Property / cites work: Truly Modular (Co)datatypes for Isabelle/HOL / rank @@
+Normal rank
@@ Property / cites work @@
+Foundational (co)datatypes and (co)recursion for higher-order logic
+Normal rank
@@ Property / cites work @@
+Mechanizing the Metatheory of Sledgehammer
@@ Property / cites work: Mechanizing the Metatheory of Sledgehammer / rank @@
+Normal rank
@@ Property / cites work @@
+Cardinals in Isabelle/HOL
@@ Property / cites work: Cardinals in Isabelle/HOL / rank @@
+Normal rank
@@ Property / cites work @@
+Unified Classical Logic Completeness
@@ Property / cites work: Unified Classical Logic Completeness / rank @@
+Normal rank
@@ Property / cites work @@
+Foundational extensible corecursion: a proof assistant perspective
+Normal rank
@@ Property / cites work @@
+Soundness and completeness proofs by coinductive methods
+Normal rank
@@ Property / cites work @@
+Q5667469
@@ Property / cites work: Q5667469 / rank @@
+Normal rank
@@ Property / cites work @@
+The locally nameless representation
@@ Property / cites work: The locally nameless representation / rank @@
+Normal rank
@@ Property / cites work @@
+Parametric higher-order abstract syntax for mechanized semantics
+Normal rank
@@ Property / cites work @@
+Categorical combinators
@@ Property / cites work: Categorical combinators / rank @@
+Normal rank
@@ Property / cites work @@
+Q3024831
@@ Property / cites work: Q3024831 / rank @@
+Normal rank
@@ Property / cites work @@
+Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
+Normal rank
@@ Property / cites work @@
+Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison
+Normal rank
@@ Property / cites work @@
+Programs Using Syntax with First-Class Binders
@@ Property / cites work: Programs Using Syntax with First-Class Binders / rank @@
+Normal rank
@@ Property / cites work @@
+The cartesian closed bicategory of generalised species of structures
+Normal rank
@@ Property / cites work @@
+A new approach to abstract syntax with variable binding
+Normal rank
@@ Property / cites work @@
+A general mathematics of names
@@ Property / cites work: A general mathematics of names / 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 @@
+A formalized general theory of syntax with bindings
+Normal rank
@@ Property / cites work @@
+A framework for defining logics
@@ Property / cites work: A framework for defining logics / rank @@
+Normal rank
@@ Property / cites work @@
+Towards Self-verification of HOL Light
@@ Property / cites work: Towards Self-verification of HOL Light / rank @@
+Normal rank
@@ Property / cites work @@
+Q3883467
@@ Property / cites work: Q3883467 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2726288
@@ Property / cites work: Q2726288 / rank @@
+Normal rank
@@ Property / cites work @@
+Modules over monads and initial semantics
@@ Property / cites work: Modules over monads and initial semantics / rank @@
+Normal rank
@@ Property / cites work @@
+Proving and applying program transformations expressed with second-order patterns
+Normal rank
@@ Property / cites work @@
+Q4552763
@@ Property / cites work: Q4552763 / rank @@
+Normal rank
@@ Property / cites work @@
+Model theory for infinitary logic. Logic with countable conjunctions and finite quantifiers
+Normal rank
@@ Property / cites work @@
+GMeta: A Generic Formal Metatheory Framework for First-Order Representations
+Normal rank
@@ Property / cites work @@
+A universe of binding and computation
@@ Property / cites work: A universe of binding and computation / rank @@
+Normal rank
@@ Property / cites work @@
+Java and the Java Memory Model — A Unified, Machine-Checked Formalisation
+Normal rank
@@ Property / cites work @@
+A proof theory for generic judgments
@@ Property / cites work: A proof theory for generic judgments / rank @@
+Normal rank
@@ Property / cites work @@
+Q3992568
@@ Property / cites work: Q3992568 / rank @@
+Normal rank
@@ Property / cites work @@
+Secure Communicating Systems
@@ Property / cites work: Secure Communicating Systems / rank @@
+Normal rank
@@ Property / cites work @@
+Concrete Semantics
@@ Property / cites work: Concrete Semantics / rank @@
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+Q3999860
@@ Property / cites work: Q3999860 / rank @@
+Normal rank
@@ Property / cites work @@
+Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations
+Normal rank
@@ Property / cites work @@
+Proof Pearl: De Bruijn Terms Really Do Work
@@ Property / cites work: Proof Pearl: De Bruijn Terms Really Do Work / rank @@
+Normal rank
@@ Property / cites work @@
+The foundation of a generic theorem prover
@@ Property / cites work: The foundation of a generic theorem prover / rank @@
+Normal rank
@@ Property / cites work @@
+Q5714442
@@ Property / cites work: Q5714442 / rank @@
+Normal rank
@@ Property / cites work @@
+Alpha-structural recursion and induction
@@ Property / cites work: Alpha-structural recursion and induction / rank @@
+Normal rank
@@ Property / cites work @@
+Call-by-name, call-by-value and the \(\lambda\)-calculus
+Normal rank
@@ Property / cites work @@
+A canonical locally named representation of binding
+Normal rank
@@ Property / cites work @@
+Automatically Generated Infrastructure for De Bruijn Syntaxes
+Normal rank
@@ Property / cites work @@
+Incremental Pattern-Based Coinduction for Process Algebra and Its Isabelle Formalization
+Normal rank
@@ Property / cites work @@
+Recursion principles for syntax with bindings and substitution
+Normal rank
@@ Property / cites work @@
+Proving Concurrent Noninterference
@@ Property / cites work: Proving Concurrent Noninterference / rank @@
+Normal rank
@@ Property / cites work @@
+Formalizing Probabilistic Noninterference
@@ Property / cites work: Formalizing Probabilistic Noninterference / rank @@
+Normal rank
@@ Property / cites work @@
+Term-generic logic
@@ Property / cites work: Term-generic logic / rank @@
+Normal rank
@@ Property / cites work @@
+F-ing modules
@@ Property / cites work: F-ing modules / rank @@
+Normal rank
@@ Property / cites work @@
+Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions
+Normal rank
@@ Property / cites work @@
+Nonfree Datatypes in Isabelle/HOL
@@ Property / cites work: Nonfree Datatypes in Isabelle/HOL / rank @@
+Normal rank
@@ Property / cites work @@
+Primitive recursion for higher-order abstract syntax
+Normal rank
@@ Property / cites work @@
+Ott: Effective tool support for the working semanticist
+Normal rank
@@ Property / cites work @@
+Substitution revisited
@@ Property / cites work: Substitution revisited / rank @@
+Normal rank
@@ Property / cites work @@
+An algebraic generalization of Frege structures -- binding algebras
+Normal rank
@@ Property / cites work @@
+Parallel reductions in \(\lambda\)-calculus
@@ Property / cites work: Parallel reductions in \(\lambda\)-calculus / rank @@
+Normal rank
@@ Property / cites work @@
+Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving
+Normal rank
@@ Property / cites work @@
+Nominal techniques in Isabelle/HOL
@@ Property / cites work: Nominal techniques in Isabelle/HOL / rank @@
+Normal rank
@@ Property / cites work @@
+A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+Barendregt’s Variable Convention in Rule Inductions
+Normal rank
@@ Property / cites work @@
+General Bindings and Alpha-Equivalence in Nominal Isabelle
+Normal rank
@@ Property / cites work @@
+Automated Deduction – CADE-20
@@ Property / cites work: Automated Deduction – CADE-20 / rank @@
+Normal rank
@@ Property / Wikidata QID @@
+Q128037242
@@ Property / Wikidata QID: Q128037242 / rank @@
+Normal rank