PoplMark

swMATH10109MaRDI QIDQ22078

No author found.

Described by source

• Theorem Proving in Higher Order Logics

Related Items (66)

Formalizing mathematical knowledge as a biform theory graph: a case study ⋮ GMeta: A Generic Formal Metatheory Framework for First-Order Representations ⋮ Modular verification of chemical reaction network encodings via serializability analysis ⋮ Verified Analysis of List Update Algorithms. ⋮ Coq formalization of the higher-order recursive path ordering ⋮ Directly reflective meta-programming ⋮ A Rewriting Logic Approach to Type Inference ⋮ Initiality for Typed Syntax and Semantics ⋮ Mechanizing metatheory in a logical framework ⋮ A two-level logic approach to reasoning about computations ⋮ Formalizing semantic bidirectionalization and extensions with dependent types ⋮ System F in Agda, for fun and profit ⋮ αCheck: A mechanized metatheory model checker ⋮ Mechanizing type environments in weak HOAS ⋮ POPLMark reloaded: Mechanizing proofs by logical relations ⋮ 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 ⋮ Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax ⋮ Proof Pearl: De Bruijn Terms Really Do Work ⋮ Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF ⋮ Psi-calculi in Isabelle ⋮ Nominal techniques in Isabelle/HOL ⋮ Nominal Inversion Principles ⋮ Nominal Lawvere theories: a category theoretic account of equational theories with names ⋮ Strong normalization for the simply-typed lambda calculus in constructive type theory using Agda ⋮ A formalized general theory of syntax with bindings: extended version ⋮ Derivation and inference of higher-order strictness types ⋮ Multimodal Separation Logic for Reasoning About Operational Semantics ⋮ Modules over monads and initial semantics ⋮ A verified framework for higher-order uncurrying optimizations ⋮ Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison ⋮ Structural Abstract Interpretation: A Formal Study Using Coq ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A computer-verified monadic functional implementation of the integral ⋮ Programming Inductive Proofs ⋮ \(\mathrm{HO}\pi\) in Coq ⋮ The Matita Interactive Theorem Prover ⋮ Mechanizing proofs with logical relations – Kripke-style ⋮ Formalizing implicative algebras in Coq ⋮ Formalization of a polymorphic subtyping algorithm ⋮ Representing and Reasoning with Operational Semantics ⋮ Eliminating Redundancy in Higher-Order Unification: A Lightweight Approach ⋮ 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 Sound Semantics for OCaml light ⋮ Unnamed Item ⋮ A formalization of multi-tape Turing machines ⋮ The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus ⋮ Harpoon: mechanizing metatheory interactively ⋮ Formalizing Operational Semantic Specifications in Logic ⋮ Mechanizing the Metatheory of mini-XQuery ⋮ Mechanized metatheory revisited ⋮ Proof assistants: history, ideas and future ⋮ Term-generic logic ⋮ Rensets and renaming-based recursion for syntax with bindings ⋮ Free Theorems and Runtime Type Representations ⋮ Type Preservation as a Confluence Problem ⋮ 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 ⋮ Mechanizing metatheory without typing contexts

This page was built for software: PoplMark