POPLMark reloaded: Mechanizing proofs by logical relations (Q5110924): Difference between revisions

@@ 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 @@
+Unbound
@@ Property / describes a project that uses: Unbound / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / Wikidata QID @@
+Q113857457
@@ Property / Wikidata QID: Q113857457 / rank @@
+Normal rank
@@ Property / cites work @@
+Explicit substitutions
@@ Property / cites work: Explicit substitutions / rank @@
+Normal rank
@@ Property / cites work @@
+Q4681360
@@ Property / cites work: Q4681360 / rank @@
+Normal rank
@@ Property / cites work @@
+Normalization for the Simply-Typed Lambda-Calculus in Twelf
+Normal rank
@@ Property / cites work @@
+Q4995161
@@ Property / cites work: Q4995161 / rank @@
+Normal rank
@@ Property / cites work @@
+Copatterns
@@ Property / cites work: Copatterns / rank @@
+Normal rank
@@ Property / cites work @@
+On Irrelevance and Algorithmic Equality in Predicative Type Theory
+Normal rank
@@ Property / cites work @@
+A Formalized Proof of Strong Normalization for Guarded Recursive Types
+Normal rank
@@ Property / cites work @@
+Types for Proofs and Programs
@@ Property / cites work: Types for Proofs and Programs / rank @@
+Normal rank
@@ Property / cites work @@
+Q3593499
@@ Property / cites work: Q3593499 / 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 @@
+Q4281462
@@ Property / cites work: Q4281462 / rank @@
+Normal rank
@@ Property / cites work @@
+Relative Monads Formalised
@@ Property / cites work: Relative Monads Formalised / rank @@
+Normal rank
@@ Property / cites work @@
+Monads need not be endofunctors
@@ Property / cites work: Monads need not be endofunctors / rank @@
+Normal rank
@@ Property / cites work @@
+Categorical reconstruction of a reduction free normalization proof
+Normal rank
@@ Property / cites work @@
+Type theory in type theory using quotient inductive types
+Normal rank
@@ Property / cites work @@
+Q5371043
@@ Property / cites work: Q5371043 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4816996
@@ Property / cites work: Q4816996 / 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 @@
+Psi-calculi in Isabelle
@@ Property / cites work: Psi-calculi in Isabelle / rank @@
+Normal rank
@@ Property / cites work @@
+Q4825542
@@ Property / cites work: Q4825542 / rank @@
+Normal rank
@@ Property / cites work @@
+Strongly typed term representations in Coq
@@ Property / cites work: Strongly typed term representations in Coq / rank @@
+Normal rank
@@ Property / cites work @@
+Program extraction from normalization proofs
@@ Property / cites work: Program extraction from normalization proofs / 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 @@
+Friends with Benefits
@@ Property / cites work: Friends with Benefits / rank @@
+Normal rank
@@ Property / cites work @@
+Programming with binders and indexed data-types
@@ Property / cites work: Programming with binders and indexed data-types / rank @@
+Normal rank
@@ Property / cites work @@
+Mechanizing proofs with logical relations – Kripke-style
+Normal rank
@@ Property / cites work @@
+A linear logical framework
@@ Property / cites work: A linear logical framework / rank @@
+Normal rank
@@ Property / cites work @@
+Type Theory Should Eat Itself
@@ Property / cites work: Type Theory Should Eat Itself / rank @@
+Normal rank
@@ Property / cites work @@
+The gentle art of levitation
@@ Property / cites work: The gentle art of levitation / rank @@
+Normal rank
@@ Property / cites work @@
+The locally nameless representation
@@ Property / cites work: The locally nameless representation / rank @@
+Normal rank
@@ Property / cites work @@
+αCheck: A mechanized metatheory model checker
@@ Property / cites work: αCheck: A mechanized metatheory model checker / rank @@
+Normal rank
@@ Property / cites work @@
+Parametric higher-order abstract syntax for mechanized semantics
+Normal rank
@@ Property / cites work @@
+Q4525278
@@ Property / cites work: Q4525278 / rank @@
+Normal rank
@@ Property / cites work @@
+Strong normalization of substitutions
@@ Property / cites work: Strong normalization of substitutions / rank @@
+Normal rank
@@ Property / cites work @@
+A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family
+Normal rank
@@ Property / cites work @@
+Q5667469
@@ Property / cites work: Q5667469 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3024831
@@ Property / cites work: Q3024831 / rank @@
+Normal rank
@@ Property / cites work @@
+Inductive families
@@ Property / cites work: Inductive families / rank @@
+Normal rank
@@ Property / cites work @@
+Q4263867
@@ Property / cites work: Q4263867 / rank @@
+Normal rank
@@ Property / cites work @@
+Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
+Normal rank
@@ Property / cites work @@
+The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
+Normal rank
@@ Property / cites work @@
+Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions
+Normal rank
@@ Property / cites work @@
+Q4068706
@@ Property / cites work: Q4068706 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3994895
@@ Property / cites work: Q3994895 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3024835
@@ Property / cites work: Q3024835 / rank @@
+Normal rank
@@ Property / cites work @@
+Foundations of Software Science and Computational Structures
+Normal rank
@@ Property / cites work @@
+A framework for defining logics
@@ Property / cites work: A framework for defining logics / rank @@
+Normal rank
@@ Property / cites work @@
+On equivalence and canonical forms in the LF type theory
+Normal rank
@@ Property / cites work @@
+Q4417801
@@ Property / cites work: Q4417801 / rank @@
+Normal rank
@@ Property / cites work @@
+The power of parameterization in coinductive proof
+Normal rank
@@ Property / cites work @@
+Q4993349
@@ Property / cites work: Q4993349 / rank @@
+Normal rank
@@ Property / cites work @@
+Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)
+Normal rank
@@ Property / cites work @@
+CakeML
@@ Property / cites work: CakeML / rank @@
+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 @@
+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 @@
+Formalization of metatheory of the Quipper quantum programming language in a linear logic
+Normal rank
@@ Property / cites work @@
+Data structures and program transformation
@@ Property / cites work: Data structures and program transformation / rank @@
+Normal rank
@@ Property / cites work @@
+Q3328540
@@ Property / cites work: Q3328540 / rank @@
+Normal rank
@@ Property / cites work @@
+Kripke-style models for typed lambda calculus
@@ Property / cites work: Kripke-style models for typed lambda calculus / rank @@
+Normal rank
@@ Property / cites work @@
+A case study in programming coinductive proofs: Howe’s method
+Normal rank
@@ Property / cites work @@
+Contextual modal type theory
@@ Property / cites work: Contextual modal type theory / rank @@
+Normal rank
@@ Property / cites work @@
+Q2871867
@@ Property / cites work: Q2871867 / rank @@
+Normal rank
@@ Property / cites work @@
+Dependently Typed Programming in Agda
@@ Property / cites work: Dependently Typed Programming in Agda / rank @@
+Normal rank
@@ Property / cites work @@
+Linear logical relations and observational equivalences for session-based concurrency
+Normal rank
@@ Property / cites work @@
+Verifying termination and reduction properties about higher-order logic programs
+Normal rank
@@ Property / cites work @@
+Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF
+Normal rank
@@ Property / cites work @@
+A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
+Normal rank
@@ Property / cites work @@
+Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
+Normal rank
@@ Property / cites work @@
+Q2778806
@@ Property / cites work: Q2778806 / rank @@
+Normal rank
@@ Property / cites work @@
+A fresh look at programming with names and binders
+Normal rank
@@ Property / cites work @@
+A formal equational theory for call-by-push-value
@@ Property / cites work: A formal equational theory for call-by-push-value / 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 @@
+Intensional interpretations of functionals of finite type I
+Normal rank
@@ Property / cites work @@
+Proof search specifications of bisimulation and modal logics for the π-calculus
+Normal rank
@@ Property / cites work @@
+General Bindings and Alpha-Equivalence in Nominal Isabelle
+Normal rank
@@ Property / cites work @@
+Mechanizing the metatheory of LF
@@ Property / cites work: Mechanizing the metatheory of LF / 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 @@
+Binders unbound
@@ Property / cites work: Binders unbound / rank @@
+Normal rank
@@ Property / cites work @@
+Types for Proofs and Programs
@@ Property / cites work: Types for Proofs and Programs / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1017/s0956796819000170
+Normal rank
@@ Property / OpenAlex ID @@
+W2995917016
@@ Property / OpenAlex ID: W2995917016 / rank @@
+Normal rank