Materials & Requisite Knowledge - shaolintl/fstar-type-checker GitHub Wiki

Consult this page for references and advice in understanding the historical and technical background behind today's research in type systems. Certain texts, like the more mathematical ones and those on particular programming languages, are included to provide the proper context. For instance, the text in Prolog is a recommended read to accentuate, for the learner, the expressivity of the expanded logical language that serves as the basis for Prolog's higher-order counterpart.

Introduction to Mathematical Foundations

  • An Introduction to Mathematical Logic, Richard E. Hodel
  • From Sets to Types to Categories to Sets, Steve Awodey

Intro to Type Theory/Programming Languages

  • Introduction to Objective Caml, Jason Hickey
  • Programming in Prolog, William F. Clocksin, Christopher S. Mellish
  • Types and Programming Languages, Benjamin C. Pierce
  • Advanced Topics in Types and Programming Languages, Pierce
  • Introduction to Lambda Calculus, Henk Barendregt & Erik Barendsen
  • Type theory lectures series (https://www.youtube.com/watch?v=ev7AYsLljxk&t=1115s)
  • Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions, Yves Bertot, Pierre Castéran, G. Huet, C. Paulin-Mohring

Type Calculi

On Implementing HO-Logic

  • Programming with Higher-Order Logic, Dale Miller, Gopalan Nadathur

On ELPI

  • ELPI: fast, Embeddable, Prolog Interpreter, Cvetan Dunchev, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi
  • Implementing Type Theory in Higher Order Constraint Logic Programming, Guidi, Coen, Tassi