FunctionsAsProcesses

Sources for the formalization in Abella of Functions (lambda-calculus) as Processes (pi-calculus)

The formalization is documented in the paper "Formalizing Functions as Processes" by B. Accattoli, C. Sacerdoti Coen, published in the Proceedings of the Fourteenth Conference on Interactive Theorem Proving, Bialystok, Poland, July 31 - August 4, 2023.

Requirements

The formalization can be checked by the interactive theorem prover Abella, version 2.0.2.

Make can be used to run the formalization.

Contents

The two parts of the paper are formalized into the two files:

• "relating_pi_and_lsc.thm", and
• "relating_wh_and_mwh.thm".

The two "complements__..." files contain stuff that is not needed for the main theorems of the paper.

All the remaining files contain auxiliary definitions and proofs.