PoplMark
From MaRDI portal
Software:22078
swMATH10109MaRDI QIDQ22078FDOQ22078
Author name not available (Why is that?)
Cited In (66)
- Type Preservation as a Confluence Problem
- Free Theorems and Runtime Type Representations
- Multimodal Separation Logic for Reasoning About Operational Semantics
- Mechanizing the Metatheory of mini-XQuery
- Parameterized cast calculi and reusable meta-theory for gradually typed lambda calculi
- Verified Analysis of List Update Algorithms.
- Eliminating Redundancy in Higher-Order Unification: A Lightweight Approach
- Rensets and renaming-based recursion for syntax with bindings
- A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs
- A verified framework for higher-order uncurrying optimizations
- Strong normalization for the simply-typed lambda calculus in constructive type theory using Agda
- Coq formalization of the higher-order recursive path ordering
- Directly reflective meta-programming
- Mechanized metatheory revisited
- Binding Structures as an Abstract Data Type
- Initiality for Typed Syntax and Semantics
- GMeta: A Generic Formal Metatheory Framework for First-Order Representations
- Structural Abstract Interpretation: A Formal Study Using Coq
- Modular verification of chemical reaction network encodings via serializability analysis
- Mechanizing metatheory in a logical framework
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
- Mechanizing metatheory without typing contexts
- A formalized general theory of syntax with bindings: extended version
- Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison
- Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF
- The locally nameless representation
- POPLMark reloaded: Mechanizing proofs by logical relations
- A formalization of multi-tape Turing machines
- \(\mathrm{HO}\pi\) in Coq
- Mechanizing proofs with logical relations – Kripke-style
- Title not available (Why is that?)
- A list-machine benchmark for mechanized metatheory (extended abstract)
- The Matita Interactive Theorem Prover
- Nominal Lawvere theories: a category theoretic account of equational theories with names
- Mechanizing type environments in weak HOAS
- Formalizing implicative algebras in Coq
- Formalization of a polymorphic subtyping algorithm
- Modules over monads and initial semantics
- A Rewriting Logic Approach to Type Inference
- αCheck: A mechanized metatheory model checker
- A Sound Semantics for OCaml light
- Proof assistants: history, ideas and future
- Formalizing semantic bidirectionalization and extensions with dependent types
- Representing and Reasoning with Operational Semantics
- The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus
- Psi-calculi in Isabelle
- System F in Agda, for fun and profit
- A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL
- A solution to the PoplMark challenge based on de Bruijn indices
- Formal metatheory of programming languages in the Matita interactive theorem prover
- Nominal techniques in Isabelle/HOL
- A two-level logic approach to reasoning about computations
- A list-machine benchmark for mechanized metatheory
- A head-to-head comparison of de Bruijn indices and names
- Nested abstract syntax in Coq
- Explicit contexts in LF (extended abstract)
- A computer-verified monadic functional implementation of the integral
- Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention
- Derivation and inference of higher-order strictness types
- Nominal Inversion Principles
- Programming Inductive Proofs
- Harpoon: mechanizing metatheory interactively
- Term-generic logic
- Formalizing Operational Semantic Specifications in Logic
- Proof Pearl: De Bruijn Terms Really Do Work
- Formalizing mathematical knowledge as a biform theory graph: a case study
This page was built for software: PoplMark
