The following pages link to Andrej Bauer (Q390413):
Displaying 47 items.
- A non-commutative Priestley duality. (Q390415) (← links)
- On the failure of fixed-point theorems for chain-complete lattices in the effective topos (Q418812) (← links)
- Programming with algebraic effects and handlers (Q478396) (← links)
- Metric spaces in synthetic topology (Q651311) (← links)
- Sheaf toposes for realizability (Q938241) (← links)
- A constructive theory of continuous domains suitable for implementation (Q1023289) (← links)
- Analytica --- an experiment in combining theorem proving and symbolic computation (Q1272608) (← links)
- On fixed-point theorems in synthetic computability (Q1683373) (← links)
- Equilogical spaces (Q1826625) (← links)
- Multibasic and mixed hypergeometric Gosper-type algorithms (Q1974697) (← links)
- Cartesian closed categories of separable Scott domains (Q2253174) (← links)
- (Q2753674) (← links)
- On the failure of fixed-point theorems for chain-complete lattices in the effective topos (Q2805156) (← links)
- On the Bourbaki-Witt principle in toposes (Q2841501) (← links)
- First steps in synthetic computability theory (Q2852343) (← links)
- Canonical effective subalgebras of classical algebras as constructive metric completions (Q2917338) (← links)
- (Q3075211) (← links)
- Two constructive embedding‐extension theorems with applications to continuity principles and to Banach‐Mazur computability (Q3159421) (← links)
- RZ: a Tool for Bringing Constructive and Computable Mathematics Closer to Programming Practice (Q3611720) (← links)
- (Q4513573) (← links)
- SIMILARITY-BASED RELATIONS IN DATALOG PROGRAMS (Q4650073) (← links)
- (Q4737182) (← links)
- A Relationship between Equilogical Spaces and Type Two Effectivity (Q4787852) (← links)
- Propositions as [Types] (Q4823804) (← links)
- Intuitionistic Mathematics and Realizability in the Physical World (Q4907917) (← links)
- On Monadic Parametricity of Second-Order Functionals (Q4910422) (← links)
- A Relationship between Equilogical Spaces and Type Two Effectivity (Q4917046) (← links)
- Implementing Real Numbers With RZ (Q4918049) (← links)
- Stone Duality for Skew Boolean Algebras with Intersections (Q4923724) (← links)
- An extensible equality checking algorithm for dependent type theories (Q5028472) (← links)
- Equality Checking for General Type Theories in Andromeda 2 (Q5041060) (← links)
- Runners in Action (Q5041086) (← links)
- (Q5101353) (← links)
- Five stages of accepting constructive mathematics (Q5122448) (← links)
- (Q5320785) (← links)
- Every metric space is separable in function realizability (Q5377467) (← links)
- RZ: A Tool for Bringing Constructive and Computable Mathematics Closer to Programming Practice (Q5426863) (← links)
- An injection from the Baire space to natural numbers (Q5740665) (← links)
- An Effect System for Algebraic Effects and Handlers (Q5891182) (← links)
- An Effect System for Algebraic Effects and Handlers (Q5892064) (← links)
- Finitary type theories with and without contexts (Q6053849) (← links)
- The HoTT Library: A formalization of homotopy type theory in Coq (Q6278647) (← links)
- The Countable Reals (Q6528745) (← links)
- Analytica -- an experiment in combining theorem proving and symbolic computation (Q6560372) (← links)
- Incorporating a database of graphs into a proof assistant (Q6648164) (← links)
- MLFMF: Data Sets for Machine Learning for Mathematical Formalization (Q6702011) (← links)
- Comodule Representations of Second-Order Functionals (Q6746142) (← links)
