The published papers may differ from the preprint versions.

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 **. Accepted for publication. arXiv:1201.6272v1

41. (with J. Berger, H. Ishihara, P. Schuster) A predicative
completion of uniform spaces.
** Annals of Pure and Applied Logic **. In press.

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.

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.

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

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

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.

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

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

Back to my home page.

Erik Palmgren, July 15, 2011.