Nextjournal
  • Explore
  • Pricing
  • Docs
  • Try nowSignup or log in →
ExplorePricingDocsTry instantlySign up or log in →
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
© 2021 Nextjournal GmbH

Product

  • Help & Docs
  • Explore
  • Homepage
  • Changelog
  • Pricing

Company

  • About us
  • Get in touch
  • Twitter
  • Videos
  • Blog

Legal

  • Terms & Conditions
  • Privacy Policy
  • Imprint