Research papers by Ivar Rummelhoff

Polymorphic Π₁ Types and a Simple Approach to Propositions, Types and Sets

Dr.Scient.thesis submitted January 1, 2007. It consists of two independent parts. Part I is concerned with Π₁ types in system F. Part II, which is almost three times as long, has a much wider scope (and hyperlinks). Comments are welcome!

Abstract (HTML)
PDF version as printed (1.7MB)
PDF version with corrections
Corrections (HTML)

Supervisor: Dag Normann.
Doctor Scientiarum is a Norwegian PhD equivalent (soon to be abandoned).

Polynat in PER-models

Polynat is not universal in all PER-models.
Published in Theoretical Computer Science 316 (2004), pp 215-224

PDF version

Polymorphic Π₁ Types

A few results concerning polymorphic Π₁ types (types of the polymorphic lambda calculus where the quantifiers only occur positively). This was article was written in a hurry and contains some mistakes. They have been corrected in part I of my thesis, which also contains other results concerning Π₁ types.

PDF version (revised February 6, 2003)

Short Counterexample

Not every Scott domain is a retract of a product of finite domains.

PDF version (one page)

Normal Domain Representations of Topological Spaces

A subset T of a (Scott) domain D is a normal totality if it is upward closed and "total meet" is an equivalence relation on T. We prove that every topological space can be represented by a domain with normal totality.

Published in Mathematical Logic Quarterly 47 (2001), pp 409-412.
PDF version

Preparing a presentation at Institut Mittag-Leffler february 2001, I realised that the result can be slightly strengthened. This is described here (PDF, one page).

Cand.scient.thesis: Models of Polymorphism with Totality

Submitted Friday the 12th of November 1999. Supervisor: professor Dag Normann .
Candidatus scientiarum is a form of extended masters degree.

Main results

• Any topological space has a normal representation.
• The "standard model" of system F using Scott domains can be extended with five different notions of totality.
• There is a natural set of `concrete' types, such that any total element in the interpretation of one such type is represented by a term.
• A diagram F in the category of Scott domains (and e-p-pairs) is bounded if there is a cone under F. For each partial order P, there is an unbounded P-diagram iff P has a crown (in some precise sense).

total.pdf contains a PDF version of the thesis, whereas total.ps.gz contains a (gzipped) postscript version.

total_errata.ps contains a list of known errors and misprints. It was last updated September 11, 2000.