TY - GEN
T1 - Formalizing Functions as Processes
AU - Accattoli, Beniamino
AU - Blanc, Horace
AU - Coen, Claudio Sacerdoti
N1 - Publisher Copyright:
© Beniamino Accattoli, Horace Blanc, and Claudio Sacerdoti Coen; licensed under Creative Commons License CC-BY 4.0 14th International Conference on Interactive Theorem Proving (ITP 2023)
PY - 2023/7/1
Y1 - 2023/7/1
N2 - 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.
AB - 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.
KW - Abella
KW - Lambda calculus
KW - binders
KW - pi calculus
KW - proof assistants
U2 - 10.4230/LIPIcs.ITP.2023.5
DO - 10.4230/LIPIcs.ITP.2023.5
M3 - Conference contribution
AN - SCOPUS:85168769044
T3 - Leibniz International Proceedings in Informatics, LIPIcs
BT - 14th International Conference on Interactive Theorem Proving, ITP 2023
A2 - Naumowicz, Adam
A2 - Thiemann, Rene
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
T2 - 14th International Conference on Interactive Theorem Proving, ITP 2023
Y2 - 31 July 2023 through 4 August 2023
ER -