Presentation

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:

Explain concisely the general context and interest of selected research papers,
Understand and reformulate the motivations and impact of the proposed research topic,
Communicate in writing and orally the purpose of their research, using standard tools in the discipline (i.e., LaTeX manuscript and slides / poster presentations),
Master the technologies used in their field (LaTeX, git, videoconference tools, BiBTeX, markdown, etc.).

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

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′),
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].

Goals

Educational

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 research¹ 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.

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.

Timeline

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.

Tools

Will be used during this program, among other resources:

References and our document will be shared on https://github.com/CinRC/reversible-lambda,
teams will be our main method of “live” communication,
Email will be our main method of asynchronous communication.

Miscellaneous

Reservation of rights: I reserve the right to change this syllabus without limitation and without prior notice. If I do substantially modify any item or policy, I will notify you during a lecture, or send an e-mail to your augusta.edu e-mail account.
Download a pdf version of this page.
Contact: caubert@augusta.edu
Created with debian, pandoc and latex.
All my documents are under Creative Commons Attribution 4.0 International License. Sources are available upon motivated request.
You will need a pdf reader to consult some of the documents: I recommend choosing an open-source pdf reader.

References

[1]

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.

[2]

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.

[3]

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.

[4]

B.C. Pierce, Types and programming languages, MIT Press, London, England, 2002.