Map Theory is a foundation of mathematics built on top of untyped lambda calculus rather than first order predicate logic. Map Theory is constructed by taking a simple programming language (essentially untyped lambda calculus) and by adding Hilberts epsilon operator. All constructs of ZFC set theory (membership, negation, implication, and universal quantification) are definable as terms in ZFC, and all theorems of ZFC are provable in Map Theory. Map Theory is suited for reasoning about classical mathematics as well as computer programs. Furthermore, Map Theory is suited for eliminating the barrier between classical mathematics and computer science rather than just supporting the two fields side by side.

Logiweb is a system for distribution of mathematical definitions, lemmas, and proofs over the internet; it supports cooperation between researchers and allows formal verification of proofs that depend on definitions, lemmas, and other proofs that reside on different computers that are connected by the internet. The main test site for Logiweb is at logiweb.eu. There are mirrors at topps.diku.dk/logiweb and logiweb.imm.dtu.dk.

- 1992: Map theory.
- Presents a theory based on lambda calculus that has power like ZFC set theory and contains a programming language as a natural subset. In: Theoretical Computer Science vol.102, pp.1-133, 1992.
- 1997: A kappa-denotational semantics for Map Theory in ZFC+SI
- With Chantal Berline. A semantic proof of the consistency of map theory within ZFC+SI, where SI asserts the existence of an inaccessible cardinal. In: Theoretical Computer Science vol.179, pp.137-202, 1997.
- 2002: Lambda-calculus as a foundation of mathematics.
- A presentation of the semantics and syntax of a simplified version of map theory. In: Logic, Meaning and Computation : Essays in Memory of Alonzo Church.
- 2002: Map theory with classical maps.
- Essentially the same as the above, but with a lot more detail and 380kbyte of formal proofs aimed at automatic proof systems. DIKU Technical report.
- 2008: A gentle introduction to map theory
- The paper gives an introduction to map theory with pointers to other papers for mathematical details. In: New Approaches to Classes and Concepts in Volume 14 of Studies in Logic
- 2014: A synthetic axiomatization of Map Theory
- A new axiomatization of Map Theory. Also contains a good starting point for learning the theory. Submitted to Theoretical Computer Science.

- 2004: Logiweb.
- Presented at the Mathematical Knownledge Management Symposium and published in ENTCS Volume 93, pp.70-101.
- 2005: The implementation of Logiweb
- Presented at the CADE-20 workshop on Empirically Successful Classical Automated Reasoning (ESCAR).
- 2006: Logiweb - a system for web publication of mathematics
- Presented at the The Second International Congress of Mathematical Software and published in Mathematical Software - ICMS 2006, volume 4151/2006 of Lecture Notes in Computer Science, pages 343-353. Springer Berlin / Heidelberg, 2006.

- 1985: Optimal Reconstruction of Bandlimited Bounded Signals.
- The paper provides the solution to a more than 20 years old problem in sampling theory.
- 1986: Representing Signals by their Toppoints in Scale Space
- The paper proves that signals are uniquely determined by their 'toppoints', allowing a new kind of sampling.
- 1991: The Importance of Cardinality, Separability, and Compactness in Computer Science with an example from Numerical Signal Analysis
- Symposium on General Topology and Applications, Oxford.

- 1989: Arrays in Pure Functional Programming Languages
- Arrays are available in imperative programming languages but problematic in pure functional programming languages. The paper describes an associative data structure suited for pure functional programming which has tolerable access time. The data structure can be indexed by integers, in which case it functions like an array. The data structure can also be indexed by other data structures than arrays, and it stores sparse arrays efficiently.
- 2002: Dedekind completion as a method for constructing new Scott domains
- Presented at the Computing: the Australasian Theory Symposium (CATS) 2002
- 2007: Basic Operations on Preordered Coherent Spaces
- The paper proves elementary theorems about Preordered Coherent Spaces (PCSs) in a way which allows the Mizar system to do automatic verification of the proofs.
- 2014: An Actuarial Programming Language for Life Insurance and Pensions
- The paper presents a domain specific language for actuarial computations.

- 1991: Knowledge-Based Assistance for Generating and Executing Space Operations Procedures
- The Expert Operator's Associate (EOA) was a system developed for the European Space Operations Center (ESOC).
- 2009: Experimental set-up to test a 50 W helicon plasma thruster
- The paper briefly descibes the experimental setup for testing the Helicon Plasma Hydrazine Combined Micro (HPHCom) thruster, including the control system produced by Rovsing.

- 2001: Mathematics and Computation
- A textbook for first year university students that introduces many topics relevant for computer science students such as recursion, logic, quantifiers, sets, integers, real numbers and objects. The textbook uses map theory as a uniform framework for all of mathematics and computer science. Mathematics and Computation was a first year mathematics course at DIKU.

- Towards a Semantics of Emerald Expressed in Map Theory.
- An example of the specification of the semantics of a non-deterministic, parallel programming language within the framework of Map Theory. Preseented at the ECOOP'94 workshop on logical foundations of object oriented programming, Bologna, Italy, 1994.

A repository for machine readable proofs has been established December 2, 2003.

- Object oriented mathematics
- A presentation of a mathematical notation that gains rigour without sacrificing clarity.

Student projects 2005 and 2006

Course material for the course 2006/07 (in Danish).

logiweb and logiweb-announce.

Klaus Grue, December 17, 2014