PoplMark

swMATH10109MaRDI QIDQ22078FDOQ22078

Author name not available (Why is that?)

Official website: http://www.seas.upenn.edu/~plclub/poplmark/

Described by source

• Theorem Proving in Higher Order Logics

Cited In (only showing first 100 items - show all)

• A verified framework for higher-order uncurrying optimizations
• Coq formalization of the higher-order recursive path ordering
• Directly reflective meta-programming
• Mechanized metatheory revisited
• 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
• A formalized general theory of syntax with bindings: extended version
• Formalizing operational semantic specifications in logic
• The locally nameless representation
• A formalization of multi-tape Turing machines
• HYBRID
• Beluga
• Twelf
• LMNtal
• AURA
• Abella
• Bedwyr
• cminor
• LEGO
• Tac
• Gmeta
• LNgen
• Nominal Isabelle
• RepLib
• CC-Pi
• 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
• FreshML
• Modules over monads and initial semantics
• Programming inductive proofs. A new approach based on contextual types
• Reasoning with higher-order abstract syntax and contexts: a comparison
• HOL2P
• Delphin
• MiniAgda
• SPEC
• Teyjus
• Autosubst
• mini-ML
• CRSX
• Unbound
• PureScript
• Psi-calculi
• List Update Algorithms
• Sage
• Flow
• Logipedia
• Visual DSD
• A Rewriting Logic Approach to Type Inference
• 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
• Psi-calculi in Isabelle
• 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
• POPLMark reloaded: mechanizing proofs by logical relations
• A list-machine benchmark for mechanized metatheory
• metalib
• Harpoon
• 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
• Mechanizing proofs with logical relations -- Kripke-style
• Derivation and inference of higher-order strictness types
• The Matita interactive theorem prover
• Caml
• Harpoon: mechanizing metatheory interactively
• Term-generic logic
• Proof Pearl: De Bruijn Terms Really Do Work
• Formalizing mathematical knowledge as a biform theory graph: a case study
• GMeta: a generic formal metatheory framework for first-order representations
• Type Preservation as a Confluence Problem
• WANDA
• Rensets and renaming-based recursion for syntax with bindings
• The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: a proof via corresponding calculus
• Strong normalization for the simply-typed lambda calculus in constructive type theory using Agda
• Multimodal Separation Logic for Reasoning About Operational Semantics
• Mechanizing metatheory without typing contexts
• Verified analysis of list update algorithms
• Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF
• Free theorems and runtime type representations
• \(\mathrm{HO}\pi\) in Coq
• Parameterized cast calculi and reusable meta-theory for gradually typed lambda calculi
• Title not available (Why is that?)
• A list-machine benchmark for mechanized metatheory (extended abstract)
• αCheck: A mechanized metatheory model checker
• System F in Agda, for fun and profit
• Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention
• Nominal Inversion Principles
• coq-library-undecidability
• A higher-order abstract syntax approach to verified transformations on functional programs
• Initiality for typed syntax and semantics

This page was built for software: PoplMark