The following pages link to Concrete Semantics (Q2926333):
Displaying 43 items.
- Semi-intelligible Isar proofs from machine-generated proofs (Q287340) (← links)
- Flag-based big-step semantics (Q516041) (← links)
- Amortized complexity verified (Q670702) (← links)
- Introduction to ``Milestones in interactive theorem proving'' (Q1663212) (← links)
- CoSMed: a confidentiality-verified social media platform (Q1663221) (← links)
- Verified iptables firewall analysis and verification (Q1663231) (← links)
- A verified SAT solver framework with learn, forget, restart, and incrementality (Q1663234) (← links)
- Formalization of the resolution calculus for first-order logic (Q1663242) (← links)
- A formalized general theory of syntax with bindings (Q1687739) (← links)
- An algebraic framework for minimum spanning tree problems (Q1786562) (← 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)
- Verifying minimum spanning tree algorithms with Stone relation algebras (Q1994364) (← links)
- On the semantics of polychronous polytimed specifications (Q1996008) (← links)
- Foreword to the special focus on formal proofs for mathematics and computer science (Q2018656) (← links)
- CoCon: a conference management system with formally verified document confidentiality (Q2031419) (← links)
- Formalising \(\varSigma\)-protocols and commitment schemes using crypthol (Q2031427) (← links)
- Distilling the requirements of Gödel's incompleteness theorems with a proof assistant (Q2051568) (← links)
- Isabelle's metalogic: formalization and proof checker (Q2055847) (← links)
- A unifying splitting framework (Q2055869) (← links)
- A formalization and proof checker for Isabelle's metalogic (Q2108191) (← links)
- Verifying graph programs with monadic second-order logic (Q2117269) (← links)
- CryptHOL: game-based proofs in higher-order logic (Q2175214) (← links)
- Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL (Q2209537) (← links)
- Agda formalization of a security-preserving translation from flow-sensitive to flow-insensitive security types (Q2229149) (← links)
- From LCF to Isabelle/HOL (Q2280211) (← links)
- Soundness and completeness proofs by coinductive methods (Q2362498) (← links)
- Semantic representation of general topology in the Wolfram language (Q2364674) (← links)
- A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality (Q2817909) (← links)
- Translating Scala Programs to Isabelle/HOL (Q2817953) (← links)
- CoSMed: A Confidentiality-Verified Social Media Platform (Q2829248) (← links)
- Automatic Functional Correctness Proofs for Functional Search Trees (Q2829265) (← links)
- A Consistent Foundation for Isabelle/HOL (Q2945636) (← links)
- A Linear First-Order Functional Intermediate Language for Verified Compilers (Q2945646) (← links)
- Comprehending Isabelle/HOL’s Consistency (Q2988665) (← links)
- ACKERMANN’S FUNCTION IN ITERATIVE FORM: A PROOF ASSISTANT EXPERIMENT (Q5037519) (← links)
- (Q5875431) (← links)
- (Q5875432) (← links)
- (Q6060676) (← links)
- (Q6079215) (← links)
- Unifying splitting (Q6103590) (← links)
- Binary Generalized PCP for Two Periodic Morphisms is Decidable in Polynomial Time (Q6154978) (← links)
- A formalization of the CHSH inequality and Tsirelson's upper-bound in Isabelle/HOL (Q6190081) (← links)
