Programming Language Foundations in Agdaplfa

Untyped: Untyped lambda calculus with full normalisation

published Dec 21 2019, 11:23

Inference: Bidirectional type inference

published Dec 21 2019, 11:23

Bisimulation: Relating reduction systems

published Dec 21 2019, 11:22

More: Additional constructs of simply-typed lambda calculus

published Dec 21 2019, 11:06

DeBruijn: Intrinsically-typed de Bruijn representation

published Dec 21 2019, 11:00

Lambda: Introduction to Lambda Calculus

published Dec 21 2019, 10:58

Properties: Progress and Preservation

published Dec 21 2019, 10:51

Acknowledgements

published Dec 18 2019, 16:37

Programming Language Foundations in Agda

published Dec 18 2019, 16:14

Dedication

published Dec 11 2019, 18:58

BigStep: Big-step semantics of untyped lambda calculus

published

Relations: Inductive definition of relations

published

Confluence: Confluence of untyped lambda calculus 🚧

published

Fonts

published

Equality: Equality and equational reasoning

published

Decidable: Booleans and decision procedures

published

Isomorphism: Isomorphism and Embedding

published

Induction: Proof by Induction

published

Naturals: Natural numbers

published

Lists: Lists and higher-order functions

published

Quantifiers: Universals and existentials

published

Negation: Negation, with intuitionistic and classical logic

published

Connectives: Conjunction, disjunction, and implication

published

Preface

published

Substitution: Substitution in the untyped lambda calculus

published

Statistics: Line counts for each chapter

published