Klaus Grue

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.

Mathematics and Computation

Logic repository

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

Papers

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. Published in Theoretical Computer Science vol.102, pp.1-133, 1992. Electronic version not available. For preprints, contact me.

A gentle introduction to map theory

To appear. The paper gives an introduction to map theory with pointers to other papers for mathematical details

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.

Logiweb.

Presented at the Mathematical Knownledge Management Symposium and published in ENTCS Volume 93, pp.70-101.

Lambda-calculus as a foundation of mathematics.

A presentation of the semantics and syntax of a simplified version of map theory.

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.

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. Theoretical Computer Science vol.179, pp.137-202, 1997.

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.

Object oriented mathematics

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

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.