PLFA Solution

Solution to the exercises from Programming Language Foundations with Agda: https://plfa.github.io/

Agda version: 2.8.0

Building

Type-check every solution file:

make          # or: make check
make clean    # remove _build/

The demo/ directory is excluded. Override the binary with make AGDA=/path/to/agda.

Table of Contents

Part 1

• 1. Naturals: Natural numbers (code)
• 2. Induction: Proof by Induction (code)
• 3. Relations: Inductive definition of relations (code)
• 4. Equality: Equality and equational reasoning (code)
• 5. Isomorphism: Isomorphism and Embedding (code)
• 6. Connectives: Conjunction, disjunction, and implication (code)
• 7. Negation: Negation, with intuitionistic and classical logic (code)
• 8. Quantifiers: Universals and existentials (code)
• 9. Decidable: Booleans and decision procedures (code)
• 10. Lists: Lists and higher-order functions (code)

Part 2

• 1. Lambda: Introduction to Lambda Calculus (code)
• 2. Properties: Progress and Preservation (code)
• 3. DeBruijn: Intrinsically-typed de Bruijn representation (code)
• 4. More: Additional constructs of simply-typed lambda calculus (code)
• 5. Bisimulation: Relating reduction systems (code)
• 6. Inference: Bidirectional type inference
• 7. Untyped: Untyped lambda calculus with full normalisation
• 8. Confluence: Confluence of untyped lambda calculus
• 9. BigStep: Big-step semantics of untyped lambda calculus

Part 3

• 1. Denotational: Denotational semantics of untyped lambda calculus
• 2. Compositional: The denotational semantics is compositional
• 3. Soundness: Soundness of reduction with respect to denotational semantics
• 4. Adequacy: Adequacy of denotational semantics with respect to operational semantics
• 5. ContextualEquivalence: Denotational equality implies contextual equivalence

Appendix

• 1. Substitution: Substitution in the untyped lambda calculus