- Category Theory for Programmers - Bartosz Milewski (book) put together by Igal Tabachnik as (online version); also available as (video lectures part I), (part 2), (part 3) and (series of blog posts)
- Categories for the lazy functional programmer - MGS 2019 - Thorsten Altenkirch (course), (MGS 2009 version - slides, solutions to exercises)
- Category Theory for Computing Science - Michael Barr, Charles Wells (book)
- Basic Category Theory - Tom Leinster (arXiv)
- Introduction to Categories and Categorical Logic - Samson Abramsky, Nikos Tzevelekos (arXiv)
- Basic Bicategories - Tom Leinster (arXiv)
- Induction, Coinduction, and Fixed Points: A Concise Comparative Survey - Moez A. AbdelGawad (arXiv)
- Mutual Coinduction - Moez A. AbdelGawad (arXiv)
- On terminal coalgebras derived from initial algebras - Jiri Adamek (arXiv)
- Category Theory Study Group (video playlist)
- Takt Category Theory - Runar Bjarnason (video playlist)
- Introduction to higher category theory - Tobias Dyckerhoff (Lecture Notes, Problem Sets)
- An Introduction to n-Categories - John C. Baez (arXiv)
- The periodic table of n-categories - Eugenia Cheng (video)
- Monoidal Categories, Higher Categories - Jamie Vicary (course notes)
- An informal introduction to topos theory - Tom Leinster (arXiv)
- Category Theory, Toposes - MathProofsable (video playlist)
- Toposes, Triples and Theories - Michael Barr, Charles Wells (pdf)
- Topos theoretic background - Olivia Caramello (paper)
- Introduction to categorical logic, classifying toposes and the bridge technique - Olivia Caramello (videos with toc)
- Toposes in Como 2018 conference: (video playlist), (slides from talks); There are introductory lectures Some glances at topos theory - Francis Borceux
- Topos à l’IHES 2015 conference: (video playlist), includes introductory: A crash course in topos theory: the big picture - André Joyal
- Higher Topos Theory - Jacob Lurie (arXiv:math/0608040)
- Seven Sketches - Brendan Fong, David I Spivak (book)
- Applied Category Theory Course forum, course material
- What is Applied Category Theory? - Tai-Danae Bradley (pdf)
- Network Models - John C. Baez, John Foley, Joseph Moeller, Blake S. Pollard (arXiv)
- A coalgebraic model of graphs - Christian Jäkel (arXiv)
- Coalgebraic Modelling Applications in Automata Theory and Modal Logic - Helle Hvid Hansen (pdf)
- Fancy Algebra - Part I: Adjoint Functors
- Applied Category Theory 2018 Workshop in Leiden (ACT 2018) (video playlist)
- Applied Category Theory 2019 (ACT 2019) (videos & summaries)
- Compositional game theory reading list - Jules Hedges (blog post)
- UCR Applied Category Theory Seminar (video playlist)
- A mathematical theory of resources - Bob Coecke, Tobias Fritz, Robert W. Spekkens arXiv:1409.5531 (application of CT for resource management)
- The Mathematical Specification of the Statebox Language - Statebox Team: Fabrizio Genovese, Jelle Herold arXiv:1906.07629 (programming language based on CT and petri nets)
- Abstraction, Composition and Contracts: A Sheaf Theoretic Approach, Alberto Speranzon, David I. Spivak, Srivatsan Varadarajan arXiv:1802.03080
- A Mathematical Theory of Co-Design - Andrea Censi arXiv:1512.08055
- Categorical Foundations for System Engineering - Spencer Breiner, Eswaran Subrahmanian, Albert Jones (paper)
- Behavioral Mereology - Brendan Fong, David Jaz Myers, David I. Spivak arXiv:1811.00420
- CQL language for RDBMS, related papers
- Theory and Applications of Categories (journal), Reprints
- Categories and General Algebraic Structures with Applications (journal)
- Journal of Functional Programming (journal)
- Programming Cafe - Bartosz Milewski (blog)
- The Comonad.Reader - Edward Kmett blog, EdK almost single handed, encoded Category Theory abstractions in Haskell, blog co authored by Gershom Bazerman, Dan Doel
- Rúnar Bjarnason blogs Apocalisp, Higher Order
- Jules Hedges blog
- A Neighborhood of Infinity - sigfpe (blog)
- Marcin Szamotulski (blog)
- Tai-Danae Bradley (blog)
This is very opinionated selection of authors that publish interesting papers about Category Theory, Type Theory and other branches of Logic, Proof Theory.
- Haskell Wiki Functional_pearls, Monads and arrows
- Philip Wadler Monads, arrows, applicatives, Parametricity
- Eugenia Cheng
- Emily Riehl
- Jacob Lurie
- Benedikt Ahrens, personal page
- Oleg Kiselyov, personal page
- Jeremy Gibbons
- Ralf Hinze
- John Hughes
- Conal Elliott, personal page
- Tarmo Uustalu
- Exequiel Rivas
- Mauro Jaskelioff
- Russell O'Connor
- Graham Hutton, University of Nottingham page
- Wouter Swierstra, Utrecht University page
- Thorsten Altenkirch, University of Nottingham page
- Robert Harper, Carnegie Mellon University
- Ulf Norell, University of Gothenburg page
- Edwin Brady, personal page
- Simon Peyton Jones, MS Reasearch page
- Samson Abramsky
- Neil Ghani
- Murdoch James Gabbay
- Robert Atkey
- Conor McBride
- Peter Dybjer, Chalmers University page
- John Baez, University of California page
- Thierry Coquand
- Martín Hötzel Escardó, University of Birmingham page
- Lucius Gregory Meredith
- André Joyal, arxiv search
- Olivia Caramello, 1, 2, 3
- Eric Finster, personal page
- Brendan Fong
- Johan Jeuring, Utrecht University page
- Martin Odersky, EPFL page
- Heather Miller
- Nada Amin, Cambridge University page
- Valery Isaev,JET Brains Research page
- Jon Sterling
- DeepSpec Summer School (2018 videos) (2017 video playlist), based on Software Foundations (book)
- The Coq proof assistant and the Mathematical Components library - Enrico Tassi (course), based on Mathematical Components (book), part of EUTypes Summer School 2018
- Basic Proof Theory — Frank Pfenning - OPLSS 2015 (video lectures, notes)
- The Coq Proof Assistant and Its Applications to Programming-Language Semantics — Adam Chlipala - OPLSS 2015 (video lectures)
- Program Verification with F* - Danel Ahman (slides, exercises)
- Advanced Topics in Programming Languages CIS 670 - Penn - Stephanie Weirich (course notes, code)
- Coq Winter School 2018
- Formalizing 100 Theorems Isabelle Coq, Top 100 Mathematical Theorems In Coq
- Iris (tutorial), (publications) Higher-Order Concurrent Separation Logic Framework implemented
Software foundations using Type Theory
- Software Foundations (Coq) (book), Idris version
- Programming Language Foundations in Agda - Philip Wadler, Wen Kokke (book)
- Practical Foundations for Programming Languages - Robert Harper (book)
- Types and Programming Languages - Frank Pfenning (course)
- Programming Languages Background - OPLSS 2017 - Robert Harper, Dan Licata (video lectures)
- Introduction to Homotopy Type Theory - EUTypes Summer School 2017 - Thorsten Altenkirch (lecture notes), (video with similar scope - Naïve Type Theory by Thorsten), (slides 2017), (slides 2018)
- Homotopy Type Theory: Univalent Foundations of Mathematics (book)
- Homotopy (type) theory - Andrej Bauer, University of Ljubljana course (github repo, videos)
- Programming in Martin-Löf's Type Theory An Introduction - Bengt Nordström, Kent Petersson, Jan M. Smith (book)
- Substructural Logics - Carnegie Mellon University - Frank Pfenning (course notes) (assignments)
- Constructive Logic - Carnegie Mellon University - Frank Pfenning (course notes) (assignments)
- Linear Logic - Carnegie Mellon University - Frank Pfenning (course)
- Computational Type Theory - OPLSS 2018 - Robert Harper (course), lecture notes, high quality videos, (video playlist) - lower quality videos
- Homotopy Type Theory - Carnegie Mellon University - Robert Harper (course) lecture notes, papers
- Computational Higher Type Theory - Carnegie Mellon University - Robert Harper (course)
- Kerodon (book about categorical homotopy theory) (book) (links)
- Dependent Types in the Idris Programming Language - OPLSS 2017 - Edwin Brady (slides, examples) (video lectures)
- Advanced Functional Programming (in Agda) - University of Strathclyde - Conor McBride (github 2017), (github 2018)
- Dependently typed programming in Agda - EUTypes Summer School 2017 - Conor McBride (github)
- Introduction to programming with dependent types in Scala (2019) - Dmytro Mitin (course), based on library ProvingGround that was used to solve Polymath 14 problem resulting in (paper)
- On Voevodsky’s Univalence principle - André Joyal (video, paper) (mathematical foundations behind HoTT and Univalence principle)
- Introduction to Homotopy Type Theory (Agda) - EUTypes Summer School 2018 - Fredrik Nordvall Forsberg (slide, exercises src)
- Introduction to Dependent Type Theory - EUTypes Summer School 2018 - Matthieu Sozeau (slides)
- Workshop: "Types, Homotopy, Type theory, and Verification" 2018 (video playlist), (schedule, abstracts, links to videos)
- FAMOUS - Foundations of Mathematics: Univalent foundations and set theory 2016 (video playlist), (videos, slides, abstracts)
- HOTTEST - Homotopy Type Theory Electronic Seminar Talks - 2018 - present (links to videos), (youtube videos)
- The New York City Category Theory Seminar (youtube videos)
- (Zwanziger) - Natural Model Semantics for Comonadic and Adjoint Modal Type Theory
- Introduction to Univalent Foundations of Mathematics with Agda - MGS 2019 - Martín Hötzel Escardó (lecture notes) (github)
- Cubical Adventures (in Agda) - University of Strathclyde - Conor McBride (video)
- Investigations into cubical type theory - Hugo Herbelin (video)
- Computational Higher Type Theory - Carnegie Mellon University - Robert Harper (course)
- mortberg/cubicaltt, (paper arxiv:1611.02108: Cubical Type Theory: a constructive interpretation of the univalence axiom - Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg, (examples), (lectures)
- mortberg/yacctt paper arXiv:1712.01800 Computational Higher Type Theory III: Univalent Universes and Exact Equality Carlo Angiuli, Kuen-Bang Hou, Robert Harper, (video): Anders Mörtberg: Yet Another Cartesian Cubical Type Theory yacctt
- Axioms for Modelling Cubical Type Theory in a Topos - Ian Orton, Andrew M. Pitts (arXiv:1712.04864)
- Cubical informal type theory: The higher groupoid structure - Bruno Bentzen (arXiv:1806.08490)
- A Specification for Dependent Types in Haskell - Stephanie Weirich, Antoine Voizard, Pedro Henrique Azevedo de Amorim, Richard A. Eisenberg (video) (paper) (repo)
- Dependent Types in Haskell: Theory and Practice - Richard A. Eisenberg (arXiv)
- DOT: Scala Types from Theory to Practice—Nada Amin (video), Type soundness proofs with definitional interpreters - Nada Amin, Tiark Rompf (paper), Dependent Object Types - Nada Amin, Martin Odersky (Ph.D. Thesis), THE ESSENCE OF SCALA - Martin Odersky (blog post) SCALING DOT TO SCALA - SOUNDNESS - Martin Odersky (blog post)
- Dotty Internals (video 1) (video 2) (video 3)
- System F in Agda, for fun and profit - James Chapman, Roman Kireev, Chad Nester, Philip Wadler (paper)
- UniMath Encoding of Category Theory using UV; combines results from:
- Univalent categories and the Rezk completion - Benedikt Ahrens, Chris Kapulkin, Michael Shulman (paper), (original repository - now merged into UniMath)
- Displayed Categories - Benedikt Ahrens, Peter LeFanu Lumsdaine (paper)
- Bicategories in Univalent Foundations - Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niels van der Weide (paper)
- HoTT book - Coq described in HoTT book
- (Cubical Agda) Univalent Categories A formalization of category theory in Cubical Agda - Frederik Hanghøj Iversen (paper), (fredefox/cat)
- (Agda) Formalisation of Restriction Categories in Agda jmchapman/restriction-categories for Introduction to restriction categories - Robin Cockett
- jmchapman/categories
- HoTT book - Ada
- School and Workshop on Univalent Mathematics 2017 (notes) (github 2017) (github 2019) based on library UniMath
- (Coq) ekmett/homotopy
- (Coq) jwiegley/category-theory
- Category Theory in Coq - Aleksandra Carvalho (pdf)
- Formalizations of category theory in proof assistants MathOverflow
- overwiev Nominal Techniques - Andrew Pitts (pdf)
- Constructive Representation of Nominal Sets in Agda - Pritam Choudhury (pdf)
- ekmett/name nominal sets in Haskell, - Edward Kmett, live coding: Haskell Live-Coding, Session 18(video)
- Equivariant ZFA and the foundations of nominal techniques - Murdoch J. Gabbay (arXiv:1801.09443)
- Nominal Henkin Semantics: simply-typed lambda-calculus models in nominal sets - Murdoch J. Gabbay, Dominic P. Mulligan (arXiv:1111.0089)
- Fast Computations on Ordered Nominal Sets - David Venhoek, Joshua Moerman, Jurriaan Rot (arXiv:1902.08414)
- Automata theory in nominal sets - Mikołaj Bojańczyk, Bartek Klin, Sławomir Lasota (arXiv:1402.0897)
- Algebraic Theories over Nominal Sets - Alexander Kurz, Daniela Petrişan, Jiří Velebil (arXiv:1006.3027)
- Atompress blog, book, WIP book
- Nominal Sets and Their Applications course - lectures, exercises
- FoPSS 2019 - Nominal Techniques (slides from talks)
- http://petrinet.org/
- Topics in Concurrency - Cambridge 2018–19 Course materials
- Foundations of Algebraic Theories and Higher Dimensional Categories - Soichiro Fujii (arxiv:1903.07030)
- A unified framework for notions of algebraic theory - Soichiro Fujii (paper)
- https://github.com/statebox/tbpt
- Bialgebraic Semantics for String Diagrams - Filippo Bonchi, Robin Piedeleu, Pawel Sobocinski, Fabio Zanasi (arXiv:1906.01519)
- Bialgebraic Semantics for Logic Programming - Filippo Bonchi, Fabio Zanasi (arXiv:1502.06095)
- Programming Language Theory - Steven Shaw
- LIPICS Leibniz International Proceedings in Informatics
- statebox/awesome-applied-ct
- FP Course, Brian McKenna teaching this course (video playlist)
- Let's Lens, Tony Morris teaching this course at LambdaConf 2017 (video)
- Applied Haskell
- Nikolai Kudasov - Building a Telegram Bot in Haskell - λC 2018 (video playlist)
- Alejandro Serrano Mena - A Hands on Tutorial to Generic Programming in Haskell (video)
- FP Complete tutorial for libraries
- CIS 552: Advanced Programming (Fall 2017) - Stephanie Weirich (lecture notes) (assignments)
- CIS 194: Introduction to Haskell (Spring 2013) - Brent Yorgey (course)
- Haskell ITMO course at CTD