Project Ideas

Please feel free to get in touch, if you would like to discuss any of the topics listed below or any other ideas related to automata theory, programming languages and verification. The projects are not set in stone and can be tailored to individual interests. I have grouped them below to identify (roughly) their relationship to wider areas of computer science.

Call-By-Push-Value

Call-by-push-value (CBPV) is a programming language paradigm that, surprisingly, breaks down the call-by-value and call-by-name paradigms into simple primitives. The aim of the project is to understand the essence of the paradigm and to present the semantics of a simple CBPV programming language using regular expressions (in the spirit of the third reference).

Required skills

Interest in programming language semantics. Competence in automata theory (regular expressions). Students with a knowledge of category theory may find this project appealing.

References

1. P. B. Levy. A tutorial on call-by-push-value, 2018.
2. F. Pfenning. Lecture notes on Call-by-Push-Value, 2016.
3. S. Abramsky. Algorihtmic game semantics: a tutorial introduction, 2001.

DPDA Equivalence

Two pushdown automata (PDA) are equivalent if they accept the same language. The problem of deciding whether two given PDA are equivalent is known to be undecidable. However, it becomes decidable when the two automata are deterministic. It took 30 years to find an algorithm that, given two deterministic PDA, will be able to determine whether or not they are equivalent. The first one was given in 1997 by Geraud Senizergues, who was subsequently awarded the Goedel Prize for the result. Senizergues' original algorithm has since been considerably simplified by other researchers.

The primary objective of this project will be to understand the latest simplification due to Jancar (cited below) and implement the algorithm in several special cases to understand its complexity. The complexity of the general case is still an open problem, which would be more suitable for a DPhil project.

Required skills

This is a challenging project focussed on a cutting-edge problem in theoretical computer science. An excellent grasp of automata theory and enthusiasm for exploring the latest techniques in the area are essential.

References

1. Petr Jancar. Decidability of DPDA Language Equivalence via First-Order Grammars, 2018.

Finitely Generated Types

This project concerns the simply-typed lambda calculus. A type A is finitely generated if there exist finitely many closed terms (not necessarily of type A) such that any closed term of type A can be obtained from these terms by repeated applications. For example, the type of Church numerals is finitely generated. It is known that many types of the lambda calculus are not finitely generated (among others, the so-called monster type), but the argument that this is the case is highly indirect. The purpose of the project would be to survey how such situations are handled in various branches of mathematics and try to deploy analogous ideas in the lambda calculus to obtain a simpler argument.

Required skills

Enthusiasm for the lambda calculus and strong proof skills are essential.

References

1. Thierry Joly. The Finitely Generated Types of the Lambda-Calculus. Proceedings of TLCA 2001, Lecture Notes in Computer Science, Volume 2044, pp. 240–252, 2001.
2. H. Barendregt, W. Dekkers, R. Statman. Lambda Calculus with Types. Cambridge University Press, 2013.

Higher-Order References

The ability to store ground-type values, such as integers or booleans, is the staple of imperative programming. However, many programming languages, e.g. OCaml or Python, make it possible to store more complicated values, notably functions. This feature is often called higher-order state or general references. The purpose of the project is to understand category-theoretic properties relevant to this paradigm, and to use them to validate a number of equivalences found in the literature, e.g. Lemmata 8-10 in the second reference.

Required skills

Enthusiasm for higher-order computation, category theory and programming language semantics.

References

1. S. Abramsky, K. Honda and G. McCusker. A fully abstract game semantics for general references. Proceedings of LICS'98, pp 334-344, 1998.
2. A. S. Murawski and N. Tzevelekos. Deconstructing General References via Game Semantics. Proceedings of FOSSACS'13, Lecture Notes in Computer Science 7794, pp 241-256, 2013.

Logical Relations

Logical relations are an established technique for proving properties of lambda terms and, more broadly, programming languages involving higher-order types (not necessarily purely functional). Among others, they can be used to show that the simply-typed lambda calculus is strongly normalising or to support equivalence proofs for programs, such as those needed to validate compiler transformations. Two programs are equivalent if and only if they can be used interchangeably without affecting the result. The aim of the project is to explore the logical relations technique and automate some of its aspects.

Required skills

This project is related to the lambda calculus and principles of programming languages. It will attempt to transfer techniques from computer-aided formal verification to the setting of higher-order programming languages.

References

1. Lau Skorstengaard. An Introduction to Logical Relations (Proving Program Properties Using Logical Relations). Notes from Amal Ahmed's summer school course, 2015.
2. A. M. Pitts and I.D.B. Stark. Operational Reasoning for Functions with Local State. In A.D. Gordon and A. M. Pitts (Eds), Higher Order Operational Techniques in Semantics, Publications of the Newton Institute (Cambridge University Press, 1998), pp 227-273.
3. Derek Dreyer, Georg Neis, Lars Birkedal. The impact of higher-order state and control effects on local relational reasoning. Journal of Functional Programming 22(4-5): 477-528 (2012).

Regularity of Pushdown Automata

The regularity problem for pushdown automata, i.e. the problem "Is the language accepted by a given pushdown automaton regular?", is undecidable. However, it turns out to be decidable for deterministic pushdown automata. The first goal of the project is to understand and implement the algorithm. The second aim is to explore whether and how it could be extended to more general scenarios, e.g. deterministic second-order pushdown automata.

Required skills

Enthusiasm for exploring automata theory.

References

1. R. E. Stearns. A regularity test for pushdown machines. Information and Control 11(3), pp 323-340, 1967.
2. L. G. Valiant. Regularity and related problems for deterministic pushdown automata. Journal of the ACM 22 (1), pp 1-10, 1975.

Security Protocols

The aim of the project is to understand the state of the art in verifying security protocols, and to try to deploy automata-theoretic methods in the area. Standard automata theory is based on finite alphabets, which is not quite suitable in this context, so the project will explore automata models over infinite alphabets.

Required skills

Good knowledge of automata theory and a liking for algorithm design.

References

1. Rohit Chadha, Vincent Cheval, Stefan Ciobaca, and Steve Kremer. Automated verification of equivalence properties of cryptographic protocols. ACM Transactions on Computational Logic, 17(4), November 2016. Listed in ACM Computing Reviews' 21st Annual Best of Computing list of notable books and articles for 2016.
2. F. Neven, T. Schwentick and V. Vianu. Finite state machines for strings over infinite alphabets. ACM Transactions on Computational Logic 5(3): 403-435 (2004)

Syntactic Control of Interference

The Syntactic Control of Interference (SCI) is a typing system for higher-order programs with state that eliminates covert interference by preventing sharing of variables between functions and their arguments. Reasoning about such programs is easier and decidable. The technical goal of the project is to understand how SCI programs are modelled using multi-tape deterministic finite state automata and to identify fragments that can be analyzed in an efficient way, possibly using simpler automata-theoretic formalisms.

Required skills

Good knowledge of automata theory and a liking for type systems and algorithm design.

References

1. James Laird. Decidability and syntactic control of interference. Theoretical Computer Science 394(1-2): 64-83 (2008)