The following pages link to Bas Spitters (Q185814):
Displaying 48 items.
- Bohrification of operator algebras and quantum logic (Q383005) (← links)
- Locatedness and overt sublocales (Q638474) (← links)
- Intuitionistic quantum logic of an \(n\)-level system (Q735205) (← links)
- Constructive pointfree topology eliminates non-constructive representation theorems from Riesz space theory (Q981685) (← links)
- A computer-verified monadic functional implementation of the integral (Q987984) (← links)
- A topos for algebraic quantum theory (Q1048087) (← links)
- Locating the range of an operator with an adjoint (Q1397696) (← links)
- Metric Boolean algebras and constructive measure theory (Q1407569) (← links)
- The space of measurement outcomes as a spectral invariant for non-commutative algebras (Q1929295) (← links)
- Guarded cubical type theory (Q2319985) (← links)
- Strong continuity implies uniform sequential continuity (Q2573727) (← links)
- Formal Zariski topology: Positivity and points (Q2575775) (← links)
- Constructive algebraic integration theory (Q2575777) (← links)
- (Q2988057) (← links)
- THE GELFAND SPECTRUM OF A NONCOMMUTATIVE C*-ALGEBRA: A TOPOS-THEORETIC APPROACH (Q3011597) (← links)
- Type classes for mathematics in type theory (Q3094177) (← links)
- (Q3100022) (← links)
- Constructive theory of Banach algebras (Q3145957) (← links)
- A constructive proof of Simpson’s Rule (Q3145984) (← links)
- Metric complements of overt closed sets (Q3170557) (← links)
- Constructive Gelfand duality for C*-algebras (Q3183160) (← links)
- Corrigendum to: ‘A constructive view on ergodic theorems’ (Q3416123) (← links)
- Constructive analysis, types and exact real numbers (Q3431542) (← links)
- (Q3535984) (← links)
- Program Extraction from Large Proof Developments (Q3559767) (← links)
- Integrals and valuations (Q3621282) (← links)
- Located Operators (Q4787861) (← links)
- Type classes for efficient exact real arithmetic in Coq (Q4913763) (← links)
- Internal universes in models of homotopy type theory (Q4993352) (← links)
- Gelfand spectra in Grothendieck toposes using geometric mathematics (Q4995148) (← links)
- Synthetic topology in Homotopy Type Theory for probabilistic programming (Q5055499) (← links)
- Extracting functional programs from Coq, in Coq (Q5101927) (← links)
- (Q5151024) (← links)
- Computer Certified Efficient Exact Reals in Coq (Q5200110) (← links)
- Modalities in homotopy type theory (Q5208873) (← links)
- Modal dependent type theory and dependent right adjoints (Q5220184) (← links)
- Guarded Cubical Type Theory: Path Equality for Guarded Recursion (Q5278409) (← links)
- Almost periodic functions, constructively (Q5310646) (← links)
- Formal topology and constructive mathematics: the Gelfand and Stone-Yosida representation theorems (Q5310879) (← links)
- (Q5310892) (← links)
- The Picard Algorithm for Ordinary Differential Equations in Coq (Q5327365) (← links)
- A constructive proof of the Peter-Weyl theorem (Q5462987) (← links)
- A constructive view on ergodic theorems (Q5480629) (← links)
- (Q5718576) (← links)
- Sets in homotopy type theory (Q5740655) (← links)
- Developing the Algebraic Hierarchy with Type Classes in Coq (Q5747673) (← links)
- A constructive converse of the mean value theorem (Q5935893) (← links)
- The HoTT Library: A formalization of homotopy type theory in Coq (Q6278647) (← links)
