Prof. Dieter Spreen

Nationality
Germany
Period
April, 2023 - September, 2023
Award
LE STUDIUM / ATHENA Visiting Researcher 

From

University of Siegen - DE

In residence at

Fundamental Computer Science Laboratory of Orléans (LIFO) / University of Orléans, INSA Centre-Val de Loire - FR

Host scientist

Prof. Jérôme Durand-Lose

Biography

Dr. Dieter Spreen is a mathematician and computer scientist who since 2012 is an emeritus professor at the University of Siegen. He received an MSc in mathematics form the University of Cologne in 1973 and a PhD in computer science from the University of Brunswick in 1977. His PhD thesis focussed on the application of automata-theoretic methods to Markovian decision processes as they are used e.g. in operations research to model situations in economy and finance. After having received his habilitation degree from the University of Aix La Chapelle in 1984 with a thesis on problems in computability theory, he joined Siemens research laboratories in Munich where he worked till 1988 when he was appointed professor for theoretical computer science and mathematical logic at the University of Siegen. In 2004 he accepted an offer for a chair in mathematics at the University of Cape Town from where he returned to Siegen in 2005 for family reasons. After his retirement he hold a visiting research professorship at the University of South Africa in Pretoria for the years 2013 and 2014. Being back to Siegen he was coordinator of the international research project CID (Computing with Infinite Data), funded by the EU, with participating universities in Chile, France, Germany, Italy, Japan, Netherlands, New Zealand, Portugal, Russia, Singapore, Slovenia, South Korea, South Afrika, Sweden, UK, and the USA, which started in 2017 and finished just recently in March 2023.

PROJECT

A Domain-theoretic Model Construction for Coquand/Huet's Calculus of Construction

Software is produced by humans and thus error-prone. To guarantee that a software product works correctly, that is, according to the given specification, it is normally tested by using special input samples. As follows from daily experience not all errors will be found this way, leading to back-up cycles. For applications in safety-critical situations such as autonomous mobile robots or car driving systems this approach is thus insufficient: the correctness has to be mathematically proven. Given the size of such software packages, proving its correctness by hand is a tedious task. To this end interactive proof assistants have been developed that automatically generate large parts of the proof.

A popular such assistant is the Coq package. It is based on the Calculus of Constructions (CC) introduced by T. Coquand and G. Huet (1988), still one of the most powerful systems of constructive higher-type logic. 

Logical propositions are usually constructed from certain constants and variables with help of logical connectives like “and” and “or”. CC allows also infinitary operations. Consider e.g. the following proposition A(n)

If n is a natural number written in decimal notation on the number plate of a car and its last two digits are 95, the car is registered in Paris.

Then the collection of these formulas A(n) is a family of propositions indexed by natural numbers n, and the statement

For all n, A(n) obtained by universal quantification over the natural numbers is a new proposition. Its construction is an example of an infinitary operation.

CC allows the construction of such propositions where the family of propositions is indexed by the proofs of some proposition, but also if the propositions in CC are used as indices.

Similar constructions exist on the level of operations, where operations are e.g. constructions of propositions. More generally, there can also be constructions of operations from given ones.

Operations are classified according to the kind of which they are. Prop is one such kind: the kind of all propositions, i.e. operations without input.

So, CC consists of the following three tiers:

                                                    ProofsPropositionsKinds.

Therefore, a model construction for CC involves giving meaning to proofs, propositions, and kinds, respectively, in such a way that the rules of the calculus hold.

It is the aim of the project to give a model construction that is easy to understand and avoids foundational problems that appear e.g. when models become too large. A further goal is to show that the objects of the construction, in particular the operations, are computable.