Preface To The Special Issue For The Fifth Workshop On Formal Topology | 0 | 0.34 | 2019 |
Categories with families and first-order logic with dependent sorts. | 0 | 0.34 | 2019 |
Formal continuity implies uniform continuity near compact images on metric spaces. | 1 | 0.41 | 2014 |
A generalized cut characterization of the fullness axiom in CZF. | 0 | 0.34 | 2013 |
Double sequences, almost Cauchyness and BD-N. | 2 | 0.45 | 2012 |
A Note On Brouwer'S Weak Continuity Principle And The Transfer Principle In Nonstandard Analysis | 0 | 0.34 | 2012 |
Constructivist and structuralist foundations: Bishop's and Lawvere's theories of sets. | 5 | 0.48 | 2012 |
A predicative completion of a uniform space. | 2 | 0.41 | 2012 |
Proof-relevance of families of setoids and identity in type theory | 2 | 0.52 | 2012 |
Introduction: The philosophy of logical consequence and inference. | 0 | 0.34 | 2012 |
Metric complements of overt closed sets. | 2 | 0.45 | 2011 |
Open Sublocales Of Localic Completions | 2 | 0.39 | 2010 |
Resolution of the uniform lower bound problem in constructive analysis | 2 | 0.71 | 2008 |
Regular universes and formal spaces | 3 | 0.65 | 2006 |
Maximal and partial points in formal spaces | 7 | 1.19 | 2006 |
Binary Refinement Implies Discrete Exponentiation. | 4 | 0.54 | 2006 |
Coequalisers of formal topology | 0 | 0.34 | 2005 |
Constructive completions of ordered sets, groups and fields | 2 | 0.58 | 2005 |
Internalising modified realisability in constructive type theory | 1 | 0.47 | 2005 |
Quotient Spaces and Coequalisers in Formal Topology | 6 | 0.62 | 2005 |
A categorical version of the Brouwer–Heyting–Kolmogorov interpretation | 1 | 0.36 | 2004 |
Type theories, toposes and constructive set theory: predicative aspects of AST | 29 | 3.03 | 2002 |
Metric Boolean algebras and constructive measure theory | 6 | 1.74 | 2002 |
An Intuitionistic Axiomatisation of Real Closed Fields. | 7 | 1.19 | 2002 |
Intuitionistic choice and classical logic | 7 | 3.75 | 2000 |
An Effective Conservation Result for Nonstandard Arithmetic | 3 | 0.60 | 2000 |
Wellfounded trees in categories | 40 | 3.35 | 2000 |
Hyperfinite Type Structures | 1 | 0.40 | 1999 |
Inaccessibility in constructive set theory and type theory | 13 | 2.08 | 1998 |
Developments in constructive nonstandard analysis | 12 | 1.46 | 1998 |
Minimal Models of Heyting Arithmetic | 11 | 1.91 | 1997 |
A Logical Presentation of the Continuous Functionals | 0 | 0.34 | 1997 |
A sheaf-theoretic foundation for nonstandard analysis | 5 | 1.36 | 1997 |
Constructive Sheaf Semantics | 9 | 1.56 | 1997 |
A constructive approach to nonstandard analysis | 10 | 2.11 | 1995 |
Logically Presented Domains | 0 | 0.34 | 1995 |
The Friedman-Translation For Martin-Lofs Type Theory | 1 | 0.41 | 1995 |
A Note On Mathematics Of Infinity | 1 | 0.70 | 1993 |
Denotational Semantics of Constraint Logic Programming — A Nonstandard Approach | 2 | 0.49 | 1993 |
An Information System Interpretation of Martin-Löf′s Partial Type Theory with Universes | 4 | 0.74 | 1993 |
Remarks on Martin-Löf's Partial Type Theory | 3 | 0.64 | 1992 |
Type-theoretic interpretation of iterated, strictly positive inductive definitions | 8 | 1.29 | 1992 |
A Construction of Type: Type in Martin-Löf's Partial Type Theory with One Universe | 1 | 0.43 | 1991 |
Domain interpretations of martin-löf’s partial type theory | 18 | 2.95 | 1990 |