Pages that link to "Item:Q1722645"
From MaRDI portal
The following pages link to From types to sets by local type definition in higher-order logic (Q1722645):
Displaying 14 items.
- A verified implementation of the Berlekamp-Zassenhaus factorization algorithm (Q1984794) (← links)
- Distilling the requirements of Gödel's incompleteness theorems with a proof assistant (Q2051568) (← links)
- A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory (Q2102926) (← links)
- A formalization of the Smith normal form in higher-order logic (Q2102950) (← links)
- Setoid type theory -- a syntactic translation (Q2176677) (← links)
- Axiomization of passage from “local” structure to “global” object (Q4033508) (← links)
- (Q4508295) (← links)
- (Q5028480) (← links)
- Quotients of Bounded Natural Functors (Q5048992) (← links)
- Reasoning About Algebraic Structures with Implicit Carriers in Isabelle/HOL (Q5049005) (← links)
- Simple Type Theory is not too Simple: Grothendieck’s Schemes Without Dependent Types (Q5094472) (← links)
- Combining higher-order logic with set theory formalizations (Q6161232) (← links)
- A formalization of the CHSH inequality and Tsirelson's upper-bound in Isabelle/HOL (Q6190081) (← links)
- Verifying a sequent calculus Prover for first-order logic with functions in Isabelle/HOL (Q6611963) (← links)
