2 Reading List

2.1 Pragmatics, Practical, General Intro

Concepts in Programming Languages. Mitchell
Principles of Programming Languages. Tennent
Introduction to the Theory of Programming Languages. Meyer
Introduction to the Theory of Programming Languages. Dowek, Levy
Principles of Programming Languages. Dowek
Programming Language Concepts (2nd Ed). Sestoft
Programming Language Linguistics. Gelernter
Programming Language Theory and its Implementation - Applicative and Imperative Paradigms. Gordon
Dynamically Typed Languages. Laurence Tratt
On Understanding Types, Data Abstraction, and Polymorphism. Cardelli, Wegner
Programming Language Explorations (2nd ed). Toal, Strieker, Berardini
An Introduction to Data Types. Cleaveland

Types and Programming Languages. Pierce
Essentials of Programming Languages. Friedman, Wand
Theories of Programming Languages. Reynolds
Practical Foundations for Programming Languages. Harper
The Formal Semantics of Programming Languages - An Introduction. Winskel
Foundations for Programming Languages. Mitchell
Concepts and Semantics of Programming Languages - A Semantical Approach with OCaml and Python. Hardin et al
Concepts and Semantics of Programming Languages - Modular and Object-Oriented Constructs with OCaml, Python, C++, Ada, and Java. Hardin et al
Semantics of Programming Languages. Tennent
Semantics of Programming Languages - Structures and Techniques. Gunter
The Structure of Typed Programming Languages. Schmidt
Abstract Computing Machines - A Lambda Calculus Perspective. Kluge
Design Concepts in Programming Languages. Tubak, Gifford, Sheldon
Understanding Programming Languages. Cliff B Jones
Computation and Deduction. Pfenning
Programming Language Foundations. Aaron Stump
The Foundations of Program Verification. Loeckx, Sieber
Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. Cousot, Cousot

Type Systems for Programming Languages. Harper
Martin-Loef’s Type Theory. Norstroem, Petersson, Smith
Programming in Martin-Loef’s Type Theory - An Introduction. Norstroem, Petersson, Smith
Intuitionistic Type Theory. Per Martin-Loef
Homotopy Type Theory - Univalent Foundations of Mathematics
Proofs and Types. Girard, Taylor, Lafont
Constructive Logics - Part I: A Tutorial on Proof Systems and Typed \(\Lambda\)-Calculi. Jean Gallier
Do-it-Yourself Type Theory. Backhouse, Chisholm, Malcolm, Saaman
On the Meaning and Construction of the Rules in Martin-Loef’s Theory of Types
Propositions and Specifications of Programs in Martin-Loef’s Type Theory. Norstroem, Smith
Derivation of a Parsing Algorithm in Martin-Loef’s Theory of Types. Chisholm
Propositions as Types. Philip Wadler
Constructive Mathematics and Computer Programming. Martin-Loef
Introduction to Generalized Type Systems. Barendregt
Polymorphic Typing of an Algorithmic Language. Xavier Leroy
Typed Lambda Calculus / Calculus of Constructions. Brandl
Treatise on Intuitionistic Type Theory. Granstroem
Type Theory and Formal Proof. Nederpelt, Guevers

Set Theory for Computing Science. Glynn Winskel
Proof and Disproof in Formal Logic. Bornat
Introduction to Computation - Haskell, Logic, and Automate. Sannella, Fourman, Peng, Wadler
The Computer Modelling of Mathematical Reasoning. Alan Bundy
Modelling Puzzles in First Order Logic. Groza

Intuitionistic Logic. Dirk Van Dalen
On The Meanings of the Logical Constants and the Justifications of the Logical Laws. Per Martin-Loef
Natural Deduction - A Proof-theoretical Study. Prawitz
Natural Deduction. Tennant
Logic and Computation - Interactive Proof with Cambridge LCF. Paulson
Axiomatic Method and Category Theory. Rodin

Program = Proof (Agda). Samuel Mimram
Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Bertot, Castéran
Mathematical Components (Coq). Mahboubi, Tassi.

Lectures on the Curry-Howard Isomorphism. Sorensen
Derivation and Computation - Taking the Curry-Howard Correspondence Seriously. Simmons
Adapting Proofs-as-Programs - The Curry-Howard Protocol. Poernomo, Crossley, Wirsing
Natural Deduction and the Curry-Howard Isomorphism. Andreas Abel

Programs and Proofs - Mechanizing Mathematics with Dependent Types, Lecture Notes (Coq). Ilya Sergey
Certified Programming with Dependent Types (Coq). Chlipala
Dependently Typed Programming in Agda. Ulf Norell, James Chapman
Type-driven Development with Idris. Edwin Brady