List of Publications of Erik Palmgren

The published papers may differ from the preprint versions.

Journal Publications:

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.

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

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

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

32. (with Peter Aczel, Laura Crosilla, Hajime Ishihara, Peter Schuster) Binary refinement implies discrete exponentiation. Studia Logica, 84 (2006), 361 - 368.

31. (with Hajime 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 Peter 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 Th. 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. Abstract.

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:

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.

9. (with Sten 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.

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

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

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

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:

• (with J. Berger, H. Ishihara, P. Schuster) A predicative completion of uniform spaces, submitted for publication.
• Remarks on the relation between families of setoids and identity in type theory, Institut Mittag-Leffler report 36, 2009/2010, fall.
• Constructivist and structuralist foundations: Bishop's and Lawvere's theories of sets, Institut Mittag-Leffler report 4, 2009/2010, fall.
• (with T. Coquand and B. Spitters) Metric complements of overt closed sets, June 18, 2009.
• 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 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:

• 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 brief, first introduction to the foundations of constructive mathematics.)

Erik Palmgren, April 2, 2010.