Pages that link to "Item:Q3612442"
From MaRDI portal
The following pages link to Constructive Type Classes in Isabelle (Q3612442):
Displaying 14 items.
- Programming and automating mathematics in the Tarski-Kleene hierarchy (Q406433) (← links)
- Linear quantifier elimination (Q707743) (← links)
- A verified ODE solver and the Lorenz attractor (Q1663218) (← links)
- CoSMed: a confidentiality-verified social media platform (Q1663221) (← links)
- From types to sets by local type definition in higher-order logic (Q1722645) (← links)
- A consistent foundation for Isabelle/HOL (Q1739913) (← links)
- A formalization and proof checker for Isabelle's metalogic (Q2108191) (← links)
- Exploring the structure of an algebra text with locales (Q2209550) (← links)
- From LCF to Isabelle/HOL (Q2280211) (← links)
- Locales: a module system for mathematical theories (Q2352487) (← links)
- Formalizing complex plane geometry (Q2354913) (← links)
- A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem (Q2362109) (← links)
- Automating change of representation for proofs in discrete mathematics (extended version) (Q2364883) (← links)
- Formal power series (Q5891671) (← links)
