Publications of Erik Palmgren

Many publications in the listing below are Open Access. The remaining publications are available in full text here, but protected by a password for copyright reasons:

Journal Publications

51. Categories with families and first-order logic with dependent sorts. Annals of Pure and Applied Logic,, 2019, doi . [ArXiV]

50. Constructive examination of a Russell style ramified type theory. Bulletin of Symbolic Logic , Volume 24, Issue 1 March 2018 , pp. 90 - 106.

49. Constructions of categories of setoids from proof-irrelevant families. Archive for Mathematical Logic vol 26 (2017), pp 51 - 66. Open Access.

48. (with Douglas S. Bridges and Matthew Hendtlass) A Constructive Examination of Rectifiability. Journal of Logic and Analysis vol 8 (2016) [PDF]

47. (with Olov Wilander) Constructing categories and setoids of setoids in type theory. Logical Methods in Computer Science. 10(2014), Issue 3, paper 25. [PDF]

46. Formal continuity implies uniform continuity near compact images on metric spaces. Mathematical Logic Quarterly 60 (2014), 66 - 69.

45. (with L. Crosilla and P. Schuster) A generalized cut characterization of the fullness axiom in CZF. Logic Journal of the IGPL 21 (2013), no. 1, 63 - 76.

44. A note on Brouwer's weak continuity principle and the transfer principle in nonstandard analyis. Journal of Logic and Analysis 3(2012).

43. (with J. Berger and D.S. Bridges) Double sequences, almost Cauchyness and BD-N. Logic Journal of the IGPL (2012) 20(1): 349-354 doi:10.1093/jigpal/jzr045

42. Constructivist and Structuralist Foundations: Bishop's and Lawvere's Theories of Sets. Annals of Pure and Applied Logic 163(2012), 1384 -1399. (Preprint version: arXiv:1201.6272v1).

41. (with J. Berger, H. Ishihara, P. Schuster) A predicative completion of uniform spaces. Annals of Pure and Applied Logic . 163(2012), 975 - 980.

40. Proof-relevance of families of setoids and identity in type theory. Archive for Mathematical Logic 51(2012), 35-47.

39. (with T. Coquand and B. Spitters) Metric complements of overt closed sets, Mathematical Logic Quarterly 57(2011), 373 - 378.

38. Open sublocales of localic completions. Journal of Logic and Analysis. 2(2010), 1 - 22.

37. Resolution of the uniform lower bound problem in constructive analysis. Mathematical Logic Quarterly, 54 (2008), 65 - 69.

36. Locally cartesian closed categories without chosen constructions. Theory and Applications of Category Theory, 20 (2008), 5 - 17. [PDF]

35. Ickestandardanalys och historiska infinitesimaler. Normat 55(2007), 166 - 176. (In Swedish.) [PDF]

34. A constructive and functorial embedding of locally compact metric spaces into locales. Topology and its Applications, 154 (2007), 1854 - 1880. [PDF]

33. (with S. Vickers) Partial Horn logic and cartesian categories. Annals of Pure and Applied Logic, 145(2007), 314-355.

32. (with P. Aczel, L. Crosilla, H. Ishihara, P. Schuster) Binary refinement implies discrete exponentiation. Studia Logica, 84 (2006), 361 - 368.

31. (with H. Ishihara) Quotient topologies in constructive set theory and type theory. Annals of Pure of Applied Logic, 141 (2006), 257 - 265.

30. Regular universes and formal spaces. Annals of Pure of Applied Logic, 137 (2006), 299 - 316.

29. Maximal and partial points in formal spaces. Annals of Pure of Applied Logic, 137 (2006), 291 - 298.

28. (with P. Schuster) Apartness and formal topology, New Zealand Journal of Mathematics, 34 (2005), 1 - 8.

27. Quotient spaces and coequalisers in formal topology. Journal of Universal Computer Science, 11 (2005), 1996 - 2007.

26. Internalising modified realisability in constructive type theory, Logical Methods in Computer Science, vol. 1, iss.2(2005), pp. 1 - 7.

25. Constructive completions of ordered sets, groups and fields. Annals of Pure and Applied Logic, 135 (2005), 243 - 262.

24. A categorical version of the Brouwer-Heyting-Kolmogorov interpretation. Mathematical Structures in Computer Science, 14 (2004), 57-72.

23. (with T. Coquand) Metric boolean algebras and constructive measure theory, Archive for Mathematical Logic, 41 (2002), 687-704.

22. An intuitionistic axiomatisation of real closed fields. Mathematical Logic Quarterly 48(2002), 297-299. (Remark: revised version of A note on constructive real closed fields. )

21. (with I. Moerdijk) Type Theories, Toposes and Constructive Set Theory: Predicative Aspects of AST, Annals of Pure and Applied Logic 114(2002), 155 - 201.

20. Real numbers in the topos of sheaves over the category of filters, Journal of Pure and Applied Algebra 160(2001), 275 - 284.

19. (with I. Moerdijk) Wellfounded trees in categories, Annals of Pure and Applied Logic 104(2000), 189 - 218.

18. Constructive nonstandard representations of generalized functions, Indagationes Mathematicae N.S. 11(1), 129 - 138, March 30, 2000.

17. An effective conservation result for nonstandard arithmetic, Mathematical Logic Quarterly 46(2000), 17 - 23.

16. (with T. Coquand) Intuitionistic choice and classical logic, Archive for Mathematical Logic, 39(2000), 53 - 74. Abstract.

15. (with D. Normann and V. Stoltenberg-Hansen) Hyperfinite Type Structures, Journal of Symbolic Logic, 64(1999), 1216 - 1242.

14. (with M. Rathjen (main author) and E.R. Griffor) Inaccessibility in constructive set theory and type theory, Annals of Pure and Applied Logic, 94(1998), 181-200.

13. Developments in constructive nonstandard analysis. Bulletin of Symbolic Logic, 4(1998), 233-272.

12. (with I. Moerdijk) Minimal models of Heyting arithmetic, Journal of Symbolic Logic 62(1997), 1448 - 1460.

11. (with V. Stoltenberg-Hansen) A logical presentation of the continuous functionals, Journal of Symbolic Logic 62(1997), 1021 - 1034.

10. Constructive sheaf semantics, Mathematical Logic Quarterly 43(1997), 321 - 327. Abstract.

9. A sheaf-theoretic foundation for nonstandard analysis, Annals of Pure and Applied Logic 85(1997), 69 - 86.

8. The Friedman-translation for Martin-Löf's type theory, Mathematical Logic Quarterly 41(1995), 314 - 326. Abstract.

7. A constructive approach to nonstandard analysis, Annals of Pure and Applied Logic 73(1995), 297 - 325.

6. A note on 'Mathematics of Infinity', Journal of Symbolic Logic 58(1993), 1195-1200.

5. An information system interpretation of Martin-Löf's partial type theory with universes, Information and Computation 106(1993), 26-60. Abstract.

4. Type-theoretic interpretation of strictly positive, iterated inductive definitions, Archive for Mathematical Logic 32(1992), 75-99.

3. (with V. Stoltenberg-Hansen) Remarks on Martin-Löf's partial type theory, BIT 32(1992), 70-83.

2. A construction of Type:Type in Martin-Löf's partial type theory with one universe, Journal of Symbolic Logic 56(1991), 1012-1015. (Earlier preprint version available here. )

1. (with V. Stoltenberg-Hansen) Domain interpretations of Martin-Löf's partial type theory, Annals of Pure and Applied Logic 48(1990), 135-196.

Publications in Conference Proceedings and Collection Volumes

11. On equality of objects in categories in constructive type theory. 23rd International Conference on Types for Proofs and Programs, Art. No. 7, 7 pp., LIPIcs. Leibniz Int. Proc. Inform., 104, Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern, 2018. [PDF]

10. From intuitionistic to formal topology: some remarks on the foundations of homotopy theory. In: Logicism, Intuitionism and Formalism - what has become of them? (eds. S. Lindström, E. Palmgren, K. Segerberg and V. Stoltenberg-Hansen), Springer 2009, 237-253. [PDF]

9. (with S. Lindström). Introduction: The Three Foundational Programmes. In: Logicism, Intuitionism and Formalism - what has become of them? (eds. S. Lindström, E. Palmgren, K. Segerberg and V. Stoltenberg-Hansen), Springer 2009, 1-22.

8. Intuitionistic Ramified Type Theory. In: Oberwolfach Reports, vol 5, issue 2, 2008, 943-946. [PDF].

7. Predicativity problems in point-free topology. In: V. Stoltenberg-Hansen and J. Väänänen eds. Proceedings of the Annual European Summer Meeting of the Association for Symbolic Logic, held in Helsinki, Finland, August 14-20, 2003, Lecture Notes in Logic 24, ASL, AK Peters Ltd, 2006. (Refereed proceedings.)

6. Continuity on the real line and in formal spaces. In: L. Crosilla, P. Schuster, editors, From Sets and Types to Topology and Analysis: Towards Practicable Foundations of Constructive Mathematics , Oxford Logic Guides, Oxford University Press 2005. (Refereed collection of papers). Errata.

5. Unifying constructive and nonstandard analysis, in: U. Berger, H. Osswald, and P. Schuster, editors, Reuniting the Antipodes---Constructive and Nonstandard Views of the Continuum. Proceedings of the Symposion in San Servolo/Venice, Italy, May 17-22, 1999. Kluwer Academic Publishers, Dordrecht, 2001 (Refereed collection of papers).

4. On universes in type theory, in: G. Sambin and J. Smith (eds.) Twenty Five Years of Constructive Type Theory. Oxford Logic Guides, Oxford University Press 1998, 191-204 (refereed collection of papers). Near final version in PDF.

3. Constructive nonstandard analysis, in: A. Petry (ed.) Méthodes et analyse non standard, Cahiers du Centre de Logique, vol. 9, 1996, 69-97 (invited paper). [PDF]

2. (with V. Stoltenberg-Hansen) Logically presented domains, in: Proc. IEEE Symposium on Logic in Computer Science '95, Washington D.C., Computer Society Press, 1995, 455-463 (refereed proceedings). Abstract.

1. Denotational semantics of constraint logic programs - a nonstandard approach, in: B. Mayoh, E. Tyugu, J. Penjam (eds.) Constraint Programming, NATO ASI Series F, Springer-Verlag, 1994, 261-288 (invited paper).

Edited work

6. T. Coquand, M.E. Maietti, and E. Palmgren (eds.). Special issue for The Fifth Workshop on Formal Topology. Journal of Logic and Analysis, vol. 11 (2019).

5. S. Awodey, N. Gambino and E. Palmgren (eds.) Special Issue: From type theory and homotopy theory to Univalent Foundations of Mathematics. Mathematical Structures of Computer Science, Volume 25 (2015), Issue 05.

4. M.E. Maietti, E. Palmgren and M. Rathjen (eds.) Special issue In Honor of Giovanni Sambin's 60th Birthday. Annals of Pure and Applied Logic 164 (2013), issue 4.

3. S. Lindström, E. Palmgren and D. Westerståhl (eds.) Special issue on The Philosophy of Logical Consequence and Inference in Synthese 187 (2012), issue 3.

2. P. Dybjer, S. Lindström, E. Palmgren and G. Sundholm (Eds.) Epistemology versus Ontology: Essays on the Philosophy and Foundations of Mathematics in Honour of Per Martin-Löf, (Logic, Epistemology and the Unity of Science Series, New York/Dordrecht: Springer Verlag.) Springer 2012.

1. S. Lindström, E. Palmgren, K. Segerberg and V. Stoltenberg-Hansen (Eds.) Logicism, Intuitionism and Formalism: What Has Become of Them? Synthese Library vol. 341. Springer 2009.

Expository writing

3. (with Peter Dybjer) Intuitionistic Type Theory, The Stanford Encyclopedia of Philosophy (Winter 2016 Edition), Edward N. Zalta (ed.), URL =

2. (with Douglas Bridges) Constructive Mathematics, The Stanford Encyclopedia of Philosophy (Winter 2013 Edition), Edward N. Zalta (ed.), URL =

1. Oavgörbara problem om ord och tal. Ingår i volymen Människor och matematik - läsebok för nyfikna. (Red. O. Helenius och K. Wallby). Nationellt Centrum för Matematikutbildning 2008. (In Swedish.)

Preprints and Technical Reports

Unpublished Notes

Preliminary versions of papers

Formalised mathematics and software

Lecture Notes and Slides

Back to my home page.

Erik Palmgren, September 15, 2019.