| Departments |
Computer Science
|
|---|
| Description | Hillebrand and Kanellakis uncovered in 1992 a striking connection between the simply-typed λ-calculus (STLC) and automata: languages defined by finite-state automata over alphabet, say, {0,1} and by λ-terms of type ((A -> A) -> (A -> A) -> A) -> Bool coincide. The proof uses an elegant semantic evaluation argument. This connection was then refined and further exploited by specialists of linear logic and automata to tackle harder problem related to higher-model checking and infinite trees, but there are few sources that focus on the case of regular languages.
The goal of this project would be to revisit the basic proof of Hillebrand and Kanellakis in the context of the linear λ-calculus. The project would be purely theoretical, the main goal being to produce an accessible introduction to the topic. A few possible further scientific goals would be:
- Determine optimal bound for the λ-term-to-automata translation in various contexts (varying with the types we allow for the term and whether we allow for non-determinism/alternation in the automata model)
- Write a proper proof of Claim 1.4.4 https://nguyentito.eu/thesis.pdf
- Formalize the results in a proof assistant and play with the extraction mechanisms |
|---|
| Preparation | Please come talk to me if you intend to pick this project. It would require you to understand some theoretical computer science you are not taught in undergrad modules at Swansea University.
Familiarity with the simply-typed λ-calculus and finite-state automata would be required. A nice starting point to check that would be to write a full proof of Hillebrand and Kanellakis' theorem on your own (see Theorem 1.1.4 and a proof sketch p18 of https://nguyentito.eu/thesis.pdf).
I would naturally put a strong focus on the refinements based on intuitionistic linear logic, so looking at that and the aspects related to its denotational semantics would be helpful. One (long) text that gives an overview of much more material than what we'd need is https://www.irif.fr/~mellies//papers/panorama.pdf.
For a large sample of the aforementioned further works that can be regarded as extensions of Hillebrand and Kanellakis' theorem, one may consult http://research.grellois.fr/doc/these.pdf and https://nguyentito.eu/thesis.pdf |
|---|
| Project Categories |
January Cohort, Theorical Computer Science |
|---|
| Project Keywords |
Logic, Programming Languages |
|---|
Level of Studies
|
| Level 6 (Undergraduate Year 3) |
yes
|
|---|
| Level 7 (Masters) |
yes
|
|---|
| Level 8 (PhD) |
yes
|
|---|