| 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 |
