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 = https://plato.stanford.edu/archives/win2016/entries/type-theory-intuitionistic.

2. (with Douglas Bridges) Constructive Mathematics, The Stanford Encyclopedia of Philosophy (Winter 2013 Edition), Edward N. Zalta (ed.), URL = http://plato.stanford.edu/archives/win2013/entries/mathematics-constructive/.

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

• A note on Brouwer's weak continuity principle and the transfer principle in nonstandard analysis. Preprint 2011.
• Remarks on the relation between families of setoids and identity in type theory, Institut Mittag-Leffler report 36, 2009/2010, fall. Revised version: Proof-relevance of families of setoids and identity in type theory. Some Coq-files with proofs.
• Constructivist and structuralist foundations: Bishop's and Lawvere's theories of sets, Institut Mittag-Leffler report 4, 2009/2010, fall. Revised version.
• Open sublocales of localic completions. U.U.D.M. Report 2009:1
• A note on domain representability and formal topology. Revised version of U.U.D.M. Report 2007:28
• Resolution of uniform lower bound problem in constructive analysis. U.U.D.M. Report 2007:11
• Locally cartesian closed categories without chosen constructions. U.U.D.M. Report 2006:36
• A constructive and functorial embedding of locally compact metric spaces into locales. U.U.D.M. Report 2006:25
• From intuitionistic to point-free topology. U.U.D.M. Report 2005:47.
• (with Steve J. Vickers) Partial Horn logic and cartesian categories. U.U.D.M. Report 2005:36
• Quotient spaces and coequalisers in formal topology. (Expanded version of: Coequalisers in formal topology. U.U.D.M. Report 2005:17.)
• (with Hajime Ishihara) Quotient topologies in constructive set theory and type theory. U.U.D.M. Report 2005:13.
• (with Peter Schuster) Apartness and formal topology. U.U.D.M. Report 2004:49 .
• Predicativity problems in point-free topology. revised version of U.U.D.M. Report 2003:43.
• Internalising modified realisability in constructive type theory U.U.D.M. Report 2004:42. (Submitted). [Associated Agda-files can be accessed here.]
• Continuity on the real line and in formal spaces. September 23, 2003. Revised version of U.U.D.M. Report 2003:32.
• Groupoids and local cartesian closure. July 2, 2003. U.U.D.M Report 2003:21. (Paper presented at PSSL 79, Doorn.)
• Constructive completions ordered sets, groups and fields U.U.D.M. Report 2003:5.
• A categorical version of the Brouwer-Heyting-Kolmogorov interpretation. (revised version of Mittag-Leffler institute preprint no 16, 2000/2001.)
• A direct proof that certain reduced products are countably saturated, U.U.D.M. Report 1994:27, 7 pp.
• Transfinite hierarchies of universes, U.U.D.M. Report 1991:7, 16 pp.

Unpublished Notes

• A Proposal for a Constructive Tarski-Grothendieck Set Theory 1 pp, February 28, 2019.
• CZF is not cowellpowered 1 pp, September 27, 2014.
• A small variation of Aczel's Relation Reflection Scheme. 1 pp., May 14, 2007.
• Partial algebras in type theory. 2 pp., June 24, 2002.
• Overspill and countable saturation implies LLPO, 1 p., March 25, 2000.
• Consequences of cut elimination for coherent theories 1 p, May 8, 1998.

Preliminary versions of papers

Formalised mathematics and software

• Modified realisability and program extraction in Martin-Löf type theory
• Formal proof of existence of minimal cover relations. An appendix to Regular universes and formal spaces (Agda/Alfa)

• Haskell program for computing fundamental groups of simplicial complexes. Download Hugs source file (a text file, see instructions in the preamble).

Lecture Notes and Slides

• Lecture Notes on Type Theory. Notes for an advanced level course, Fall term 2013.
• Category Theory and Structuralism. Seminar at SCAS, March 3, 2009.
• Locally compact spaces and formal topology.
• From intuitionistic to pointfree topology. Pure and Applied Logic Colloquium, Carnegie Mellon University, March 31, 2005.
• Regular universes and formal spaces, slides for seminar talks in Uppsala and Göteborg, spring 2002.
• Topics in Domain Theory and Point-free Topology 48 pp. U.U.D.M. Lecture Notes 2002:LN2. Errata. (Supplementary lecture notes for the course Domänteori MN1.) Addendum, Nov. 22.
• Suddig logik och gitter 8 pp. (In Swedish. Very basic introduction to fuzzy sets as examples of lattices for second year students.)
• Konstruktiv logik 40 pp. U.U.D.M. Lecture Notes 2002:LN1. (Lecture notes in Swedish for the course Tillämpad logik DV1.)
• Constructing order completions in type theory, slides for a talk at the Dagstuhl seminar on Verification and Constructive Algebra, Jan. 5 - 10, 2003.
• Constructive mathematics, 12 pp., August 22, 1997. Lectures notes for Copenhagen Logic Summer School, 11 - 22 August, 1997. (This is a very brief, first introduction to the foundations of constructive mathematics.)

Erik Palmgren, September 15, 2019.