pcf-lean is a formalization of the denotational semantics of PCF in Lean, following the notes of the 2023-2024 Denotational Semantics course at Cambridge (as written by Andrew Pitts, Glynn Winskel, Marcelo Fiore, and Meven Lennon-Bertrand).
This presentation encodes the denotations of PCF terms as ω-cocontinuous monotone maps taking environments to semantic values.
This formalization adopts an intrinsically-typed and intrinsically-scoped representation of PCF syntax, based on the technique described in PLFA (Philip Wadler, Wen Kokke, and Jeremy G. Siek). The approach taken to proving the undefinability of parallel OR is described by Kurt Sieber in "Reasoning about sequential functions via logical relations".
While this project intends to faithfully follow the proofs written in the course, some aspects have been changed for ease of formalization. Most notably, rather than prove an extensionality principle for the contextual preorder in terms of syntactic functions, we prove one in terms of evaluation contexts, requiring the extension of the formal approximation relation to evaluation contexts. This also affects the proof of full abstraction failure, which has been reworked to use this new extensionality principle instead.
The contents of this formalization are best viewed interactively through a Lean installation, such as the official VSCode extension for Lean 4, which allows users to step through proofs and jump between definitions. Nevertheless, some effort has been made to document or otherwise structure the code to be as readable as possible without the interactivity of a theorem prover (except where it hasn't; contributions welcome!).
| File | Description |
|---|---|
| Utility.lean | Basic vocabulary for the formalization. |
| File | Description |
|---|---|
| Syntax.lean | The core syntax of PCF: types, contexts, variables, and terms. |
| Substitution.lean | Renamings and substitutions for variables and terms. |
| File | Description |
|---|---|
| Evaluation.lean | Characterizing PCF terms with unique evaluations. |
| Context.lean | Term contexts and contextual equivalence. |
| File | Description |
|---|---|
| Order.lean | Partial orders and monotonicity. |
| Domain.lean | Domains (pointed ω-CPOs), continuity, and fixed points. |
| Flat.lean | Flat domains. |
| File | Description |
|---|---|
| Denotation.lean | Denotations of syntactic objects. |
| Approximation.lean | Formal approximation between semantics and syntax. |
| Soundness.lean | Soundness, compositionality, and adequacy of denotations. |
| Extensionality.lean | Extensionality principles for contextual equivalence. |
| Undefinability.lean | Undefinable denotations and full abstraction failure. |