Pages that link to "Item:Q2879246"

The following pages link to Truly Modular (Co)datatypes for Isabelle/HOL (Q2879246):

Displaying 34 items.

• Formal verification of an executable LTL model checker with partial order reduction (Q682350) (← links)
• CoSMed: a confidentiality-verified social media platform (Q1663221) (← links)
• Formalization of the resolution calculus for first-order logic (Q1663242) (← links)
• A formalized general theory of syntax with bindings (Q1687739) (← links)
• Markov chains and Markov decision processes in Isabelle/HOL (Q1701041) (← links)
• A formalized general theory of syntax with bindings: extended version (Q1984791) (← links)
• Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL (Q1984795) (← links)
• Non-well-founded deduction for induction and coinduction (Q2055840) (← links)
• A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory (Q2102926) (← links)
• CryptHOL: game-based proofs in higher-order logic (Q2175214) (← links)
• Deep induction: induction rules for (truly) nested types (Q2200833) (← links)
• Interactive verification of architectural design patterns in FACTum (Q2335950) (← links)
• A decision procedure for (co)datatypes in SMT solvers (Q2360873) (← links)
• Soundness and completeness proofs by coinductive methods (Q2362498) (← links)
• Automatic refinement to efficient data structures: a comparison of two approaches (Q2417948) (← links)
• Probabilistic Functions and Cryptographic Oracles in Higher Order Logic (Q2802495) (← links)
• Translating Scala Programs to Isabelle/HOL (Q2817953) (← links)
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL (Q2938044) (← links)
• A Formalized Hierarchy of Probabilistic System Types (Q2945633) (← links)
• Deriving Comparators and Show Functions in Isabelle/HOL (Q2945654) (← links)
• Friends with Benefits (Q2988636) (← links)
• Quotients of Bounded Natural Functors (Q5048992) (← links)
• (Q5111307) (← links)
• Coinduction in Flow: The Later Modality in Fibrations (Q5875348) (← links)
• (Q5875411) (← links)
• (Q5875419) (← links)
• (Q5875441) (← links)
• Effect polymorphism in higher-order logic (proof pearl) (Q5915785) (← links)
• A comprehensive framework for saturation theorem proving (Q5918558) (← links)
• Effect polymorphism in higher-order logic (proof pearl) (Q5919584) (← links)
• A comprehensive framework for saturation theorem proving (Q5970776) (← links)
• Into the Infinite - Theory Exploration for Coinduction (Q6108814) (← links)
• Proofs about Network Communication: For Humans and Machines (Q6197375) (← links)
• Linear resources in Isabelle/HOL (Q6552504) (← links)