Thesis

• Herbrand, Jacques. Recherches sur la théorie de la démonstration. 1930.

Blogs

• Lawrence Paulson
• Kihong Heo (in Korean)
• Derek Dreyer
• PL Enthusiast
• PL Perspectives

Cryptography

Cryptographic Protocols

• Veronique Cortier
• MPRI
• Berry Schoenmakers
• MPRI2

Cryptography

• The Joy of Cryptography
• Alessandro Chiesa
• Mihir Bellare
• Rafael Pass
• Alex Ozdemir
• Dakshita Khurana
• Boaz Barak
• Riccardo Pucella
• Vipul Goyal

Computer-Aided Cryptography

• Marco Gaboardi
• CAPS-Workshop
• Riccardo Pucella
• Tamarin Book

Post-Quantum

• Dominique Unruh

Quantum

• Matt Amy
• Steven Herbert
• Edinburgh
• Nottingham

Category Theory

Institution Theory, Algebraic Specification

• Tarlecki
• Institution Independent Model Theory
• Tutorial on Institution Theory

Coalgebra & Semantics

• Jurriaan Rot
• Peter Aczel

Type Theory & Curry-Howard-Lambek Isomorphism & HoTT

(Dependent) Type Theory

• Carlo Angiuli
• Typechecker-zoo

(Category-theoretic) Semantics

• Meseguer

HoTT

• Introduction to Univalent Foundations of Mathematics with Agda
• HoTT Course (Andrej Bauer)
• Intro to HoTT (Egbert Rijke)
• Cubical TT

Programming

• Category Theory for Programming

Automated Resoning & Automated Theorem Proving

Term Rewriting & Rewriting Logic

• Meseguer

  unification & narrowing

• Meseguer2
• Jouannaud

  lecture note in french

Automated Theorem Proving

• D’Souza
• Dillig
• Farinelli

  Skolemisation, Herbrand Universe, Resolution, Paramodulation, etc

• Ringeissen
• TUM

  Herbrand, Skolem, Goedel, Decidability, …

• Contejean

  In french

• U. Innsbruck

Satisfiability

• Marijn Heule
• Theory & Practice of SMT Solving

Formal Verification & Model Checking

Formal Verification

• Masaryk U.

Model Checking

• Joost Pieter-Katoen
• Michael Blondin (in French)
• TUM
• Roderick Bloem
• UNIUD

Model Checking Tools Tutorials (Spin & NuSMV)

• U. Trento
• Karlsruhe

Model Checking & Machine Learning & Statistics

• Modeling and Verification of Probabilistic Systems, RWTH
• Formal Verification Meets Machine Learning, RWTH

Concurrency

• Damien Zufferey
• Models of concurrency, categories, and games
• Foundations of Concurrency
• Separation Logic course by Benjamin Pierce

Program Verification

• uni. Freiburg

Systems Verification

• Tej Chajed

Knowledge, Epistemology, Philosophy

(TODO) https://sites.pitt.edu/~rbrandom/Courses%201%20c.html https://jshaw.net/courses/gradlanguage.html https://mmandelkern.github.io/ https://iccl.inf.tu-dresden.de/web/Foundations_of_Logic_Programming_(WS2021)/en https://lat.inf.tu-dresden.de/~fernandez/esslli2019/unifDLsCourse.html

Formal Epistemology

• Probability and Induction
• Fundamentals of Bayesian Epistemology

Knowledge Representation and Reasoning

• IIT Delhi
• Sebastian Rudolph - Foundations of Knowledge Representation
• Meghyn Bienvenu

Modal Logic

• Frank Pfenning - Modal Logic
• Eric Pacuit - Modal Logic

=== Logic ===

Logic

• TUM
• Bodirsky Lecture Note
• mathematical logic (Marco Benini)
• Antonio Montalban
• Steve Awodey
• UIUC
• Advanced Logic
• Samuel Buss

ToC

• UIUC (Madhusudan Parthasarathy)
• Warsaw (Mikołaj Bojańczyk)

===== Misc. ===== Programming Language

• PL Classics
• Software Foundations
• Concrete Semantics
• CPDT
• PLFA
• Semantics
• PLAI

Lecture Materials

• Samuel Mimram
• Umang Mathur

(in French)

• Sémantique opérationnelle et typage

Braunschweig TCS lecture notes

• Braunschweig

Coq

• Ref Manual from FLINT group

Lean

• FP & TP in Lean4 (Stanford)
• Harry Goldstein

Rust

• Rust Programming - UPenn
• Safe System Programming

program synthesis

• mit 6.S084/6.887 2020 (Armando Solar-Lezama)
• ucsd cse-291 (Nadia Polikarpova)

Software Analysis

• Mayur Naik
• The Fuzzing Book
• The Debugging Book
• CMU
• Jihyeok Park

Distributed Systems

• DSLabs
• Lindsey Kuper

KAIST KAIST PL

Compiler

• Steve Zdancewic
• Adrian Sampson
• Mooly Sagiv

  Teaching Compilers Backward (from PL Perspective)

Cornell

• cs3110 - functional programming with ocaml
• cs4160 - formal verification
• cs6110 - advanced programming languages
• cs6112 - foundations of concurrency
• cs6117 - category theory for computer scientists
• cs6861 - Introduction to Kleene Algebra
• cs6156 - runtime verification

CMU

• Bug Catching: Automated Program Verification (Ruben Martins)
• Automated Reasoning and Satisfiability (Ruben Martins)
• Program Analysis (Jonathan Aldrich)
• rwh (Bob Harper)

OS

• MIT 6.828
• gatech CS3210 Taesoo Kim
• MIT 6.826 Principles of Computer Systems Nickolai Zeldovich
• Yale Zhong Shao (Lab: CertikOS)
• OS Dev Wiki

Deep Learning

• Foundations of Deep Learning (Soheil Feizi)
• Geometric Deep Learning
• NYU-CDS (Yann LeCun)
• Deep Learning Theory - UIUC

SNU

• Architecture

Blockchain

• Princeton
• Aggelos Kiayias
• Elaine Shi

Software Practice

• Steve Tarzia
• Full Stack Web Dev - Riccardo Pucella
• Web Browser Engineering - Pavel Panchekha

Multi Agent Systems / Game Theory

• Kate Larson

From Database Theory Community

• database theory
• Database Theory Book
• Michael Benedikt - Automata & Logic
• database theory
• Dan Suciu

From Finite Model Theory & Descriptive Complexity Community

• Finite Model Theory Lecture Note
• Nicole Schweikardt
• Tomas Jakl - Finite Model Theory, Game Comonad, etc

Optimization

• Del Pia

Latex

• Not So Short Intro To Latex

How to write papers?

• Benjamin Pierce

=== Some Articles ===

• Deduction Theorem