PoplMark
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Proof assistants: history, ideas and future
- HYBRID
- Ott
- metalib
- Harpoon
- Beluga
- TinkerType
- Derivation and inference of higher-order strictness types
- Formalizing implicative algebras in Coq
- Formalization of a polymorphic subtyping algorithm
- Twelf
- LMNtal
- The locally nameless representation
- A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL
- A solution to the PoplMark challenge based on de Bruijn indices
- Nested abstract syntax in Coq
- Formal metatheory of programming languages in the Matita interactive theorem prover
- A list-machine benchmark for mechanized metatheory
- A formalized general theory of syntax with bindings: extended version
- \(\mathrm{HO}\pi\) in Coq
- Harpoon: mechanizing metatheory interactively
- FreshML
- Rensets and renaming-based recursion for syntax with bindings
- Tac
- Bedwyr
- Abella
- LEGO
- cminor
- System F in Agda, for fun and profit
- Gmeta
- LNgen
- Strong normalization for the simply-typed lambda calculus in constructive type theory using Agda
- Mechanized metatheory revisited
- Term-generic logic
- AURA
- Mechanizing metatheory without typing contexts
- Formalizing mathematical knowledge as a biform theory graph: a case study
- A two-level logic approach to reasoning about computations
- Nominal Isabelle
- Nominal Lawvere theories: a category theoretic account of equational theories with names
- RepLib
- CC-Pi
- Binding structures as an abstract data type
- A higher-order abstract syntax approach to verified transformations on functional programs
- Explicit contexts in LF (extended abstract)
- A head-to-head comparison of de Bruijn indices and names
- A list-machine benchmark for mechanized metatheory (extended abstract)
- Modular verification of chemical reaction network encodings via serializability analysis
- GMeta: a generic formal metatheory framework for first-order representations
- Initiality for typed syntax and semantics
- Programming inductive proofs. A new approach based on contextual types
- Mechanizing the metatheory of mini-XQuery
- A Rewriting Logic Approach to Type Inference
- SPEC
- HOL2P
- MiniAgda
- Teyjus
- Delphin
- Unbound
- Autosubst
- mini-ML
- Formalizing semantic bidirectionalization and extensions with dependent types
- Proof Pearl: De Bruijn Terms Really Do Work
- Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF
- CRSX
- Nominal Inversion Principles
- Representing and Reasoning with Operational Semantics
- Eliminating Redundancy in Higher-Order Unification: A Lightweight Approach
- PureScript
- Psi-calculi
- List Update Algorithms
- Sage
- Flow
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
- Logipedia
- αCheck: A mechanized metatheory model checker
- Verified analysis of list update algorithms
- Visual DSD
- Mechanizing proofs with logical relations -- Kripke-style
- The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: a proof via corresponding calculus
- Formalizing operational semantic specifications in logic
- Parameterized cast calculi and reusable meta-theory for gradually typed lambda calculi
- Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention
- POPLMark reloaded: mechanizing proofs by logical relations
- scientific article; zbMATH DE number 7204440 (Why is no real title available?)
- Structural Abstract Interpretation: A Formal Study Using Coq
- The Matita interactive theorem prover
- Free theorems and runtime type representations
- Mechanizing metatheory in a logical framework
- Type Preservation as a Confluence Problem
- Multimodal Separation Logic for Reasoning About Operational Semantics
- A Sound Semantics for OCaml light
- Reasoning with higher-order abstract syntax and contexts: a comparison
- Psi-calculi in Isabelle
- coq-library-undecidability
- WANDA
- Caml
- A formalization of multi-tape Turing machines
- Coq formalization of the higher-order recursive path ordering
- Directly reflective meta-programming
This page was built for software: PoplMark
