Undergraduate Research

CSCI 4990 - Spring 2024

Clément Aubert & Logan Beatty

January 10, 2024


This class is aimed at fostering and developing abilities to conduct individual research in Computer Science. As such, its structure may be evolving and concrete expectations are hard to establish, but the main student learning outcomes are that students who successfully complete this course should be able to:

Research Project Presentation

In a nutshell:
As Ugo Dal Lago observed in a public message, there is no “reversible” machine capable of executing λ-terms. The goal of this course is to develop such a model of computation, using the “Non-Deterministic Abstract Machines” [1], to obtain machines capable of undoing their reductions of λ-terms (and possibly of π-calculus terms) for the first time.
In more details:
Reversible computing is gaining a lot of traction as a debugging and forensic tool, but also due to its connections to quantum and adiabatic computing [2]. We also know since the 70’s and Bennett’s trick that it is possible to “revert” any Turing Machine, in a precise technical sense [3]. The question this class will investigate is: is it possible to “revert” another fundamental model of computation, namely the λ-calculus [4]?

Answering positively this question requires to

  1. Define a reversible abstract model of computation M:
    1. Define a forward execution, i.e., rules expressing that the model M in a state s will reduce the λ-terms u to u and move to state s in one forward step :(M,s,u) → (M,s′,u′),
    2. Define a backward execution, i.e., rules expressing that the model M in a state s will reduce the λ-terms u to u and move to state s in one backward step :(M,s,u) ⇝ (M,s′,u′),
  2. Ensure that the model is “correct”:
    1. By showing that it can correctly execute forward and backward some simple examples,
    2. By proving properties such as the loop lemma, i.e., (M,s,u) → (M,s′,u′)⬌(M,s′,u′) ⇝ (M,s,u),
    3. By comparing it to existing reversible functional languages [3].

Our exploration will start with an attempt to “revert” the recently developed “Non-Deterministic Abstract Machines” [1].



The main educational goal of the project is to give to Logan the taste of a scholarly culture, and to introduce him to research questions at the intersection of Computer Sciences and Mathematics. More precisely, our goals are to:

  • Foster Logan’s independence, to sharpen his capacities to solve problems by himself.
  • Improve his self-efficacy, to believe in his capacities but also to identify when and how to ask for help.
  • Encourage his curiosity, to drive his own intellectual journey.
  • Introduce to the administrative aspects of research1 by e.g. searching for good-quality journals and venues to submit our work, or funds to sparkle other projects.
  • Become confident with technologies (git, LaTeX, references managers, markdown, …) common in research.


Our main goals, aside from the educational goals detailed above, are to produce a research document that will be shared with experts in the field through self-archiving on the arXiv.org and github repositories. All the material produced will be released under Creative Commons licenses (or similar open-source licence), to ease distribution and re-use by the community.


The program will start on January 8th and terminates on May 1st, 2024. Weekly meeting are scheduled on Wed., from 11 to 12am, in Dr. Aubert’s office.


Will be used during this program, among other resources:



M. Biernacka, D. Biernacki, S. Lenglet, A. Schmitt, Non-deterministic abstract machines, in: B. Klin, S. Lasota, A. Muscholl (Eds.), 33rd International Conference on Concurrency Theory, CONCUR 2022, September 12-16, 2022, Warsaw, Poland, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022: pp. 7:1–7:24. https://doi.org/10.4230/LIPICS.CONCUR.2022.7.
B. Aman, G. Ciobanu, R. Glück, R. Kaarsgaard, J. Kari, M. Kutrib, I. Lanese, C.A. Mezzina, L. Mikulski, R. Nagarajan, I.C.C. Phillips, G.M. Pinna, L. Prigioniero, I. Ulidowski, G. Vidal, Foundations of reversible computation, in: I. Ulidowski, I. Lanese, U.P. Schultz, C. Ferreira (Eds.), Reversible Computation: Extending Horizons of Computing - Selected Results of the COST Action IC1405, Springer, 2020: pp. 1–40. https://doi.org/10.1007/978-3-030-47361-7_1.
R. Glück, T. Yokoyama, Reversible computing from a programming language perspective, Theor. Comput. Sci. 953 (2023) 113429. https://doi.org/10.1016/J.TCS.2022.06.010.
B.C. Pierce, Types and programming languages, MIT Press, London, England, 2002.