Source: http://www2.math.uu.se/~palmgren/publicat.html
Timestamp: 2019-04-19 05:21:29+00:00

Document:
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).
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.
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.
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.
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.
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.
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).
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.
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.
From intuitionistic to point-free topology. U.U.D.M. Report 2005:47.
(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.
Continuity on the real line and in formal spaces. September 23, 2003. Revised version of U.U.D.M. Report 2003:32.
Constructive completions ordered sets, groups and fields U.U.D.M. Report 2003:5.
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.
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.
Constructing order completions in type theory, slides for a talk at the Dagstuhl seminar on Verification and Constructive Algebra, Jan. 5 - 10, 2003.
Erik Palmgren, July 15, 2011.

References: V. 
 V. 
 V. 
 V. 
 V. 
 V. 
 V. 
 V.