Lecturers: Wieb Bosma. Herman Geuvers, Alexandra Silva, Sebastiaan Terwijn and Freek Wiedijk.
Please register in blackboard for this course in order to receive (email) announcements. Relevant course information will be provided here (and not in blackboard).
Summary: What subsets of the polynomial ring F[X] are computationally enumerable, when F is a finite field? As a motivating question the following may serve: does there exist a polynomial (in many variables) for which the values (when ranging over F[X]) are precisely the irreducible polynomials of F[X]? This is the analogue of polynomials (known since Matijasevic proved that Diophantine sets over Z are computationally enumerable) that have precisely the prime numbers as their positive values. Note that the motivating question needs a more precise formulation. My brief literature search provided two clues; one, in a paper by Poonen, claiming that Diophantine sets in F[X] where not known (at least around 2003), and, interestingly, Poonen gives an argument why, contrary to conventional wisdom, the problem may be harder in the fucntion field case than in the ratinal case. Another can be found in a recent paper by Demeyer.
Summary:
Continuation calculus (CC) aims to model functional computation. It is a variation on lambda calculus and term rewriting with a more limited syntax and rules. It has been defined and studied in a paper by Geron and Geuvers [1] with the idea that evaluation in funtional programming languages can be modeled in it.
The difference with lambda calculus and term rewriting is that
- there is no choice in evaluation
- there are no bound variables
- there is no pattern matching
It has been shown how dat (numers, booleans, lists ...) can be represented in CC and how functions over these data can be defined.
Depending on the definition of the function it can be a "call-by-value" or a "call-by-nae" function. (In lambda calculus, this would be the same function, but depend on the evaluation strategy.)
In functional programming it is usual to also have "non pure" functions, using an abort, catch-throw or call/cc. In CC we can model these simply using continuations.
CC is now untyped, but it would be good to have a typed version:
- types help to specify programs and write correct programs
- data types clarify the representability of functions over data, e.g. by creating definition schemes for well-defined functions
- types may guarantee the termination: "well-typed programs always terminate"
It turned out recently that our definition of natural numbers in CC is strongly related to what is informzlly known as the "Scott numerals" in lamda calculus (as opposed to the well-known Church numerals). Scott invented these, but never published about them. They have been mentioned by Curry/Feys and Wadsworth. A recent unpublished note [2] by Abadi, Cardelli and Plotkin gives types to the Scott numerals in an extension of polymorphic lambda calculus with covariant recursive types. This gives a first proposal for typing terms in CC.
Summary: Symbolic Automata extend classical automata by using symbolic alphabets instead of finite ones. Recently, in [1] and algorithm for minimization was proposed. The aim of this project is to investigate whether the algorithm in [2] can also be adapted to symbolic automata and, more interestingly, whether there is a general methodology to adapt algorithms existent for classical automata to the setting of symbolic automata.
Summary The project consists of making a formal version (either just on paper, or maybe also using Coq) of chapter 5 of the ISO C standard. This should be a formal framework in which it is possible to talk about what a formal semantics of C is, and to relate different versions of such a semantics. The goal of the project is not to actually create such a formal semantics, just to specify what the type of such a semantics is. Input for the project are the chapter of the C standard, and the Coq files and publications of the Compcert and Formalin projects.
Links