=== Cryptographic Protocols ===

• Veronique Cortier
• MPRI
• Berry Schoenmakers
• The Joy of Cryptography
• Alessandro Chiesa

=== Term Rewriting & Rewriting Logic ===

• Meseguer

  unification & narrowing

• Meseguer2
• Jouannaud

  lecture note in french

=== Logic And Category Theory ===

• Tarlecki

=== Automated Deduction ===

• Dillig
• Farinelli

  Skolemisation, Herbrand Universe, Resolution, Paramodulation, etc

• Ringeissen
• TUM

  Herbrand, Skolem, Goedel, Decidability, …

• Contejean

  In french

• U. Innsbruck

=== Verification === Model Checking

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

Satisfiability

• Marijn Heule

Model Checking Tools Tutorials (Spin & NuSMV)

• U. Trento

Concurrency

• Damien Zufferey
• Models of concurrency, categories, and games
• Foundations of Concurrency

Program Verification

• uni. Freiburg

=== Logic ===

(Dependent) Type Theory

• Carlo Angiuli

Coalgebra

• Jurriaan Rot

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 Theory

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

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

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

KAIST KAIST PL

Compiler

• 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

CMU

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

HoTT

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

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

Cryptography

• Mihir Bellare
• Rafael Pass
• Alex Ozdemir
• Dakshita Khurana
• Boaz Barak

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

From Knowledge Representation & AI Community

• IIT Delhi
• Eric Pacuit - Modal Logic
• Sebastian Rudolph - Foundations of Knowledge Representation
• Meghyn Bienvenu

Optimization

• Del Pia

Latex

• Not So Short Intro To Latex

=== Some Articles ===

• Deduction Theorem