Klaus Grue

Research interests

Map Theory

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

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.

Papers

Papers on Map Theory

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

2016: A synthetic axiomatization of Map Theory

A new axiomatization of Map Theory. Also contains a good starting point for learning the theory. To appear in Theoretical Computer Science.

Papers on Logiweb

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.

Papers related to mathematical analysis

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.

Papers related to computer science

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.

Papers related to space

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.

Other documents

Lecture notes

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.

Workshop presentation

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.

Logic repository

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

Unpublished

Object oriented mathematics

A presentation of a mathematical notation that gains rigour without sacrificing clarity.

Links

Logiweb

Student projects 2005 and 2006

Mathematics and computation

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

Mailing list archive

logiweb and logiweb-announce.