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:

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.

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

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.

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

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

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

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

Back to my home page.

Erik Palmgren, September 15, 2019.