eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2023-07-26
5:1
5:21
10.4230/LIPIcs.ITP.2023.5
article
Formalizing Functions as Processes
Accattoli, Beniamino
1
https://orcid.org/0000-0003-4944-9944
Blanc, Horace
2
Sacerdoti Coen, Claudio
3
Inria & LIX, École Poytechnique, Palaiseau, France
Independent researcher, Paris, France
Alma Mater Studiorum - University of Bologna, Italy
We present the first formalization of Milner’s classic translation of the λ-calculus into the π-calculus. It is a challenging result with respect to variables, names, and binders, as it requires one to relate variables and binders of the λ-calculus with names and binders in the π-calculus. We formalize it in Abella, merging the set of variables and the set of names, thus circumventing the challenge and obtaining a neat formalization.
About the translation, we follow Accattoli’s factoring of Milner’s result via the linear substitution calculus, which is a λ-calculus with explicit substitutions and contextual rewriting rules, mediating between the λ-calculus and the π-calculus. Another aim of the formalization is to investigate to which extent the use of contexts in Accattoli’s refinement can be formalized.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023.5/LIPIcs.ITP.2023.5.pdf
Lambda calculus
pi calculus
proof assistants
binders
Abella