My solution to Programming Language Foundations in Agda (available at https://plfa.github.io)

The template branch contains a bare solution scaffold. You could fork this repo and use it to write your own solutions to PLFA.

[WIP]

We recommend to use ghcup to install Haskell and the package manager cabal.

Just follow the instructions on ghcup.

After the installation, you may be able to call cabal from your terminal. If you are not, consider adding following statements to your shell config file ( e.g., ~/.bashrc, ~/.zshrc).

export PATH=$HOME/.ghcup/bin:$PATH
export PATH=$HOME/.cabal/bin:$PATH

Note that it is for mac users. If you are installing Haskell on a Windows / Linux, you should modify your environment variables accordingly.

cabal v2-install --lib ieee754
cabal v2-install Agda

After a long period of compilation, you can call agda in your terminal.

• VSCode [WIP]

• Naturals(solution): Natural numbers
• Induction(solution): Proof by Induction
• Relations(solution): Inductive definition of relations
• Equality(solution): Equality and equational reasoning
• Isomorphism(solution): Isomorphism and Embedding
• Connectives(solution): Conjunction, disjunction, and implication
• Negation: Negation, with intuitionistic and classical logic
• Quantifiers: Universals and existentials
• Decidable: Booleans and decision procedures
• Lists: Lists and higher-order functions

• Lambda: Introduction to Lambda Calculus
• Properties: Progress and Preservation
• DeBruijn: Intrinsically-typed de Bruijn representation
• More: Additional constructs of simply-typed lambda calculus
• Bisimulation: Relating reduction systems
• Inference: Bidirectional type inference
• Untyped: Untyped lambda calculus with full normalisation
• Confluence: Confluence of untyped lambda calculus
• BigStep: Big-step semantics of untyped lambda calculus

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