Affiliation: Lektor (Associate Professor) until 2007,
see also my short and longer CV)
Bjerregårds Sidevej 4, DK-2500 Valby , Denmark
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.
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
- 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.
Papers on Logiweb
- 2004: Logiweb.
- Presented at the
Knownledge Management Symposium and published in ENTCS Volume 93, pp.70-101.
- 2005: The implementation of Logiweb
- Presented at the
CADE-20 workshop on
Successful Classical Automated Reasoning (ESCAR).
- 2006: Logiweb - a system for web publication
- 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)
- 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.
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
- 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
- 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.
Mathematics and computation
Course material for the course
2006/07 (in Danish).
Mailing list archive
Klaus Grue, February 25, 2014