REFERENCES.md

References

• Pi-Forall - a dependently-typed toy language that this langauge will be originally based off
• Lambda cube - a taxonomy of type systems
• nLab - awesome resource for learning category theory
• A biased history of equality in type theory - lecture notes about the differen types of equality in type theory
• Writing Your Compiler by Proving It Correct - tutorial for writing a programming langauge and proving properties about it
• Twlef - an imlementation of the LF logical framework, a λΠ-calculus
• How do you get the Calculus of Constructions from the other points in the Lambda Cube? - a very good explanation of each langauge in the lambda cube
• How is the dependent pair type analogous to a disjoint union? - great explanation of the difference between sigma and pi types and how they correspond to logic
• Foundations of Programming Languages - course that teaches programming language design and explains ABTs very well
• Practical Implementation of a Dependently Typed Functional Programming Language - very detailed tutorial for implementing dependent types
• Write You a Haskell - simply typed lambda calculus tutorial
• A tutorial implementation of a dependently typed lambda calculus - depndently typed lambda calculus tutorial
• Practical Foundations for Programming Languages - section discusses ABTs in detail
• Abstract Binding Trees in Swift - good explanation of how ABTs work
• De Bruijn index - useful to track bindings in ABT without having to deal with alpha conversion
• Unbound - a super confusing Haskell library :P
• Higher Order Abstact Syntax - binding representation
• Natural deduction - a kind of proof calculus
• Propositions as Types - amazing paper by Philip Wadler
• Bindings - Analysis of different way bindings are done and how they all "succ"
• unbound - Haskell binding package
• Simply Easy! - Really nice, easy-to-follow implementation of STLC and DTLC
• Eta-conversion - Eta conversion in definitional equality makes type checking decidable
• Elaborator Reflection - useful for understanding how holes are elaborated
• Idris language Haskell package - implementation of Idris
• Agda language Haskell package - implementation of Agda
• Pi Sigma - dependently typed language from which data definitions can be built on top
• An Idris metaprogramming "hello world" - elaborator reflection tutorial
• The Glasgow Haskell Compiler - an explanation of the design of the ghc compiler
• System FC - coercions and coercion kinds
• Rewrite rules - rewrite rules in ghc pragmas
• Hindley-Milner Inference - implementing Hindley-Milner inference in Haskell
• Hindley-Milner Type System - explains how recursion is type checked