Research project proposals by Herman Geuvers

Here is a list of topics that you may choose for a Research project (e.g. in R and D), Bachelor Thesis or Master Thesis supervised by Herman Geuvers. Please contact me if you want further details.

General Theory Projects

There are various research themes and questions that I am interested in, usually of a more theoretical nature. Here is a list of some examples, which need to be specified further; if you want to know more, please contact me.
  1. Extensions of the Turing machine or lambda calculus paradigm with "interaction", "advice" or "oracles". There is (a lot of) work on this by, for example, van Leeuwen and Wiederman, Wegner, Goldin, Smolka and many others. Many questions on the universality of these models and their relative strength remain.
  2. Operational Semantics and/or Axiomatics Semantics for programming laguages, as you've studied in "Semantiek en Correctheid" or "Semantiek en Logica".
  3. Abstracting from (2), studying Dynamic Logic or Kleene Algebra.
  4. Grammars and Automata for XML standards. What you've seen in "Talen en Automaten" for string languages can be extended to tree languages and hedge languages.
  5. Denotational semantics, for example models for type theories or models for coindcutive data types (like streams)
  6. Computation with and reasoning over infinite objects (like streams).

Education related Project

Curricula Comparison

We often hear complaints about the level of our students when they enter university or about the level they have when they have completed their Master (or Bachelor). "In the past, everything was much better ..." The goal of this project is to research whether this is true, on the basis of The point is to give a concrete inventory of A related issue of relevance may be how the total set up of the studies have cahnged or not. Has the focus changed? (E.g. from programming skills to modelling skills? Has the emphasis on mathematics changed?) It may also be interesting to study which influences (government, economy, industry, ...) have changed the studies. Here it may also be relevant to study the developments in other countries.

Formalization Projects

Stream calculus in Coq

In Coq, we can define the coinductive data type of streams, and one can define functions by "corecursion", using this data type. In Coq, a definition of an object of a coinductive type should be "guarded", which guarantees the "productivity" of the infinite object. This is quite restrictive. From (infinitary) term rewriting and co-algebra, we know various criteria for the well-definedness of infinitary objects, and we would like to include them in Coq. Another issue is the equality (bisimilarity) of two streams: when do two definitions represent the same infinite stream? We would like to have more automated support for this inside Coq. (This wil build on work of -- amond others -- Bertot, Endrullis-Hendriks-Klop, Niqui-Rutten, van der Weegen and Zantema.)

Partial recursive functions as functions over streams in Coq

We propose the following method for defining the partial recursive functions (over natural numbers) as functions from streams to streams.
  1. We consider streams over {0,S,c}, where c denotes a computation step (a tau step in proces algebra terminology), so the number n is represented by c...c S c...c S ... S c... c 0 ..., so n times a S followed by a 0, separated by c and followed by arbitrary what.
  2. A function takes streams and produces a stream; given a (code for a) partial recursive function f of arity m we define its interpretation as a function (in Coq) taking n streams and producing a stream.
  3. All this should be defined in Coq
Now we want to prove formally (in Coq), that the set of total functions is not enumerable: there is no function g that takes a (code of a) function f and returns true if f is total and false if f is not.

100 prisoners and one light bulb problem

Formalize the 100 prisoners and one light bulb problem; look here for details. There are two goals that you want a solution to have:
  1. When it terminates you want to be certain all prisoners have been in the room.
  2. Have a low expected running time.
The algorithms can get pretty complex so that computing the expected running time becomes extremely difficult. So people write simulations to estimate the expected running times to compute (2). However the simulations don't provide confidence in (1). Any broken algorithm that takes several (simulated) years to run will work in every tested case with near certainty, but the goal is to have absolute certainty. A proof is required for (1).
This is a nice example of a problem where you want to write an algorithm, and prove it's correctness (1). Then extract the algorithm and execute it to estimate (2), and compare the solutions to the puzzle.

Real time / Hybrid system verification in Coq

Embedded systems work are computer systems that typically operate in a real world environment where continuous variables (for example time, speed, temperature, ...) play a role. Interesting examples are systems (either software or hardware) that control a device on the basis of clocks and measurements of real variables in the environment. The goal of such a controller is often to keep the device within a certain state, that is, to maintain a certain invariant for the real variables.
Coq has a library of real arithmetic and calculus with which we can model the environment. We can also model the controller and prove that if it obeys certain behavioral rules, it ensures a safety requirement. So the goal is to give a formal correctness proof of a controller.

A tactic for proving primitive recursive predicates in Coq.

Together with Martijn Oostdijk, I have applied the so called `reflection method' to create a decision procedure for primitive recursive predicates (e.g. Prime(n) or Is_a_cube(n)) in the theorem prover Coq. See Proof by Computation in the Coq system, Theoretical Computer Science 272 (1-2), pp. 293 -- 314, 2001. The reflection method makes it possible to prove a predicate by computation, more precisely by computing the characteristic function.
The goal of this project is to turn the decision procedure into a full-blown tactic inside Coq. To do this, one has to be able to recognize and parse primitive recursive predicates, generate the associated characteristic functions and compute them.

Formalizing (Constructive) Analysis in Coq

Extend the CoRN repository of analysis formalized in Coq with more notions and lemmas from analysis. The CoRN repository grew out of the formalization of the Fundamental Theorem of Algebra and has later been extended by several people (most notably Luis Cruz-Filipe and Russel O'Connor) into a full blown library of constructive analysis.
What to formalize exactly is open for discussion.

Formalizing Reals in Coq

In our CoRN repository we have a constructive axiomatic description of the real numbers in Coq. There is also a classical one in the standard library of Coq. Moreover, in CoRN we have constructed the reals as Cauchy sequences of rationals and there are also other constructions. We want to exhibit different axiomatizations and study/prove their equivalence. Also we want to transfer results from the constructive world to the classical world and vice versa.

Proving the stick-sawing algorithm correct in Coq

[This is a real challenge!] If we have a number of sticks, each of length at least n and with a total length n(n+1)/2, we can saw the sticks into n pieces of lengths 1, 2, ..., n (so without glueing pieces together). This remarkable combinatorial theorem has a `proof by algorithm' [Ma, Zhou, Zhou, Combinatorica 14(3) 1994, 307--320]. We would like to formalize it and prove it correct in Coq.

Proof Assistant Technology Projects

Interactive mathematical documents from formal mathematical theories

A formalized proof in Coq encodes/represents a proof in natural deduction format. This proof can be translated into natural language, but this yields a very detailed and boring text. The obvious advantage is that the text represents a fully formalized proof and has a lot of (underlying) formal structure. The `tmegg' tool, developed and implemented in TexMacs by Lionel Mamane, attempts to integrate mathematical documents with formal proofs, by having a LaTeX style mathematical document with a Coq formalization underneath.
We want to extend tmegg with nicer and better rendering facilities and to test this basic approach to interactive mathematical documents on some larger proof developments.

Web-interfaces for proof assistants

We have developed the ProofWeb system which is a web-interface for proof assistants and can be used for Coq and Isabelle. The system also includes functionality to set-up courses, specifically also for providing exercises for a logic course. (It is used in "Beweren en Bewijzen" and has been used in various other courses.) The interface nicely renders deductions as they are created on the fly by the user via interactive commands.
There are various ways in which this interface can be enriched, e.g. by including other proof assistants like PVS.

MathWiki

The aim of the MathWiki project (funded by NWO, executed by Josef Urban and Carst Tankink) is to open up to a wider community the rich collections of knowledge stored in the repositories of proof assistants and to facilitate the extension and editing of these repositories by outside users. We plan to build a web-based collaborative authoring environment for formal mathematics, the MathWiki system. This system will provide interactive web access through a standardized interface to a number of proof assistants. The MathWiki system will also be a platform for the development of formal proofs within those proof assistants and it will provide high level access (through Wikipedia-like web pages) to their repositories of formalised mathematics. These repositories will reside on the server. and will maintain their consistency as articles are added or revised.
In the project we will study and further develop Wiki technology and semantic web technology and techniques for consistency management, all in the context of proof assistant repositories of formalized mathematics. The project thus brings together the open nature of Wiki authoring with expertise in Proof Assistants and Semantic Web technologies to build a new Wiki for mathematics, supporting content creation, search and retrieval.
From the perspective of the ordinary user of mathematics, MathWiki will be important because it will provide high-level mathematical content on the web in a much more coherent and precise way than is available at present. From the proof assistant user perspective, MathWiki will be important because it will provide an advanced environment for the collaborative authoring of verified mathematics, mediated simply by a web interface.

Type Theory Projects

Type systems for Classical Logic

The Curry-Howard formulas-as-types isomorphism is between proofs in constructive logic and typed lambda terms, which can be viewed as functional programs. Extending this isomorphism to classical logic, we can interpret classical proofs as "functional programs with jumps", which can me modeled as escape or call-cc constructs.
There has been done a lot of work on the extension of formulas-as-types to classical logic, giving rise to new presentations of the logical systems, new typed lambda calculi, new reduction rules and new reduction strategies. In all these areas (or in the combination of them) there are still many open questions left.

Type theory with explicit conversions

In the article A logical framework with explicit conversions, by H. Geuvers, F. Wiedijk (Carsten Schurmann (ed.), Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages, Cork, Ireland, ENTCS, Volume 199, 24 February 2008, Pages 33-47) we describe a type theory in which the beta-conversion is made explicit in the terms.
Various questions remain, like whether this is a practical system for doing actual proof checking or whether we can refine the system to allow only well-typed terms in teh conversion relation.

Type theory without contexts

In the article Pure Type Systems without Explicit Contexts by H. Geuvers, R. Krebbers, J. McKinna and F. Wiedijk, (Proceedings of LFMTP, workshop at FLoC 2010, Edinburgh) we describe dependent type theory (Pure Type Systems) without contexts and we prove that the context free presentation is essentially equivalent to the one with contexts. A question is whether the context free presentation makes it easier to prove properties about the system; also the extension with definitions and the implementability of such a system are open.

Fixed point combinator and Russell's paradox in inconsistent type theories

In inconsistent type theories like lambdaU, lambdaU- or lambda*, we can find a closed term of type bot. We can also find a closed term of the type of the fixed point combinator: forall A:*, (A->A)->A. It is know that we can make a looping combinator of this type, but it is an open question whether there is a fixed point combinator of this type. (It is generally believed there is none.)
Also, the proof of bot can be given in various ways, usually by interpreting some form of Burali-Forti paradox, saying that we cannot well-order the collection of all well-orderings. But can we also interpret the much simpler Russell paradox? (Stating that the collection of all sets that are not members of themselves is not a set.)