The following pages link to PoplMark (Q22078):
Displaying 49 items.
- Modular verification of chemical reaction network encodings via serializability analysis (Q288812) (← links)
- Formalizing semantic bidirectionalization and extensions with dependent types (Q347391) (← links)
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (Q438569) (← links)
- A formalization of multi-tape Turing machines (Q744986) (← links)
- Coq formalization of the higher-order recursive path ordering (Q843949) (← links)
- Directly reflective meta-programming (Q848742) (← links)
- Mechanizing type environments in weak HOAS (Q897934) (← links)
- Nominal techniques in Isabelle/HOL (Q928672) (← links)
- Modules over monads and initial semantics (Q964503) (← links)
- A verified framework for higher-order uncurrying optimizations (Q968367) (← links)
- A computer-verified monadic functional implementation of the integral (Q987984) (← links)
- Proof assistants: history, ideas and future (Q1040001) (← links)
- Derivation and inference of higher-order strictness types (Q1749138) (← links)
- Formalizing implicative algebras in Coq (Q1791188) (← links)
- Formalization of a polymorphic subtyping algorithm (Q1791209) (← links)
- The locally nameless representation (Q1945914) (← links)
- A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL (Q1945915) (← links)
- A solution to the PoplMark challenge based on de Bruijn indices (Q1945917) (← links)
- Nested abstract syntax in Coq (Q1945918) (← links)
- Formal metatheory of programming languages in the Matita interactive theorem prover (Q1945919) (← links)
- A list-machine benchmark for mechanized metatheory (Q1945921) (← links)
- A formalized general theory of syntax with bindings: extended version (Q1984791) (← links)
- \(\mathrm{HO}\pi\) in Coq (Q2031410) (← links)
- Harpoon: mechanizing metatheory interactively (Q2055903) (← links)
- Rensets and renaming-based recursion for syntax with bindings (Q2104549) (← links)
- System F in Agda, for fun and profit (Q2176683) (← links)
- Strong normalization for the simply-typed lambda calculus in constructive type theory using Agda (Q2229159) (← links)
- Mechanized metatheory revisited (Q2323447) (← links)
- Term-generic logic (Q2339466) (← links)
- Mechanizing metatheory without typing contexts (Q2352491) (← links)
- Formalizing mathematical knowledge as a biform theory graph: a case study (Q2364688) (← links)
- A two-level logic approach to reasoning about computations (Q2392484) (← links)
- Nominal Lawvere theories: a category theoretic account of equational theories with names (Q2453579) (← links)
- Binding Structures as an Abstract Data Type (Q2802464) (← links)
- A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs (Q2802499) (← links)
- Explicit Contexts in LF (Extended Abstract) (Q2804940) (← links)
- (Q2871859) (← links)
- (Q2871863) (← links)
- GMeta: A Generic Formal Metatheory Framework for First-Order Representations (Q2892744) (← links)
- Initiality for Typed Syntax and Semantics (Q2915022) (← links)
- Programming Inductive Proofs (Q3058448) (← links)
- Mechanizing the Metatheory of mini-XQuery (Q3100214) (← links)
- A Rewriting Logic Approach to Type Inference (Q3184729) (← links)
- Verified Analysis of List Update Algorithms. (Q4636599) (← links)
- Formalizing Operational Semantic Specifications in Logic (Q4982629) (← links)
- (Q5111317) (← links)
- Free Theorems and Runtime Type Representations (Q5262947) (← links)
- Type Preservation as a Confluence Problem (Q5389092) (← links)
- Multimodal Separation Logic for Reasoning About Operational Semantics (Q5415628) (← links)
