Pages that link to "Item:Q5477646"
From MaRDI portal
The following pages link to Theorem Proving in Higher Order Logics (Q5477646):
Displaying 50 items.
- PoplMark (Q22078) (← links)
- Modular verification of chemical reaction network encodings via serializability analysis (Q288812) (← links)
- Formalizing semantic bidirectionalization and extensions with dependent types (Q347391) (← links)
- ASP\(_{\text{fun}}\) : a typed functional active object calculus (Q433340) (← 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)
- 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)
- \(\mathrm{HO}\pi\) in Coq (Q2031410) (← 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)
- A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs (Q2802499) (← links)
- Explicit Contexts in LF (Extended Abstract) (Q2804940) (← links)
- Programming Inductive Proofs (Q3058448) (← links)
- Mechanizing the Metatheory of mini-XQuery (Q3100214) (← links)
- A Rewriting Logic Approach to Type Inference (Q3184729) (← links)
- Mechanized Verification of CPS Transformations (Q3498467) (← links)
- The Abella Interactive Theorem Prover (System Description) (Q3541698) (← links)
- Nominal Inversion Principles (Q3543650) (← links)
- αCheck: A mechanized metatheory model checker (Q4593089) (← links)
- Mechanizing proofs with logical relations – Kripke-style (Q4691187) (← links)
- The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus (Q4972064) (← links)
- Formalizing Operational Semantic Specifications in Logic (Q4982629) (← links)
- A type- and scope-safe universe of syntaxes with binding: their semantics and proofs (Q5019018) (← links)
- Parameterized cast calculi and reusable meta-theory for gradually typed lambda calculi (Q5020907) (← links)
- POPLMark reloaded: Mechanizing proofs by logical relations (Q5110924) (← links)
- (Q5111317) (← links)
- Structural Abstract Interpretation: A Formal Study Using Coq (Q5191090) (← links)
- The Matita Interactive Theorem Prover (Q5200015) (← links)
- Free Theorems and Runtime Type Representations (Q5262947) (← links)
- Romeo: A system for more flexible binding-safe programming (Q5371971) (← links)
- Multimodal Separation Logic for Reasoning About Operational Semantics (Q5415628) (← links)
- Psi-calculi in Isabelle (Q5890661) (← links)
