- Category Theory for Programmers - Bartosz Milewski (book) put together by Igal Tabachnik as (online version);
- 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)
- 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)
- TheCatsters videos
- VisualMath - What is...category theory?videos
- MathProofsable Category Theory videos
- 2-Dimensional Categories - Niles Johnson, Donald Yau (arxiv:2002.06055), (pdf)
- Introduction to higher category theory - Tobias Dyckerhoff (Lecture Notes, Problem Sets)
- An Introduction to n-Categories - John C. Baez (arXiv)
- Basic Bicategories - Tom Leinster (arXiv)
- The periodic table of n-categories - Eugenia Cheng (video)
- Monoidal Categories, Higher Categories - Jamie Vicary (course notes)
- Associative n-categories - Christoph Dorn (arXiv:1812.10586)
- Strictly associative and unital higher category theory - Jamie Vicary (slides)
- kerodon.net Part I - Higher category theory
- YouTube playlists:
- 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)
- Topos online 2021 conference (videos)
- 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)
- Basics in category and topos theory - David Janin
- An Introduction to Topos Theory - Ryszard Paweł Kostecki (lecture notes)
-
Seven Sketches - Brendan Fong, David I Spivak (book), Azimuth Applied Category Theory Course forum, course material
-
Functorial Data Migration - David I. Spivak (arXiv:1009.1166), Categorical Databases (video)
-
What is Applied Category Theory? - Tai-Danae Bradley (pdf)
-
Topos Institute (videos)
-
UCR Applied Category Theory Seminar (video playlist)
-
Applied Category Theory conference
- ACT 2018 (video playlist)
- ACT 2019 (videos & summaries)
- ACT 2020 conference page, (conference videos), (tutorials)
- ACT 2021 (conference recordings)
- ACT 2022 (recordings)
- ACT 2023 (recordings)
-
Polynomial Functors Course, 2021 (video playlist)
-
Workshop on Polynomial Functors, 2021 (video playlist)
-
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)
-
Compositional game theory reading list - Jules Hedges (blog post)
-
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, n-Category Cafe Blog post - John Baez
-
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 bartoszmilewski.com
- The Comonad.Reader - Edward Kmett Comonad.Reader, EdK almost single handed, encoded Category Theory abstractions in Haskell, blog co authored by Gershom Bazerman, Dan Doel
- Rúnar Bjarnason blogs: Apocalisp apocalisp.wordpress.com, Higher Order blog.higher-order.com
- A Neighborhood of Infinity - sigfpe blog.sigfpe.com
- Phil Freeman - @paf31 blog.functorial.com
- Marcin Szamotulski coot.me
- Jules Hedges julesh.com
- Bob Atkey bentnib.org
- Mathematics and Computation - Andrej Bauer http://math.andrej.com/
- Existential Type - Robert Harper (blog)
- Mathematics and Computation - Andrej Bauer (blog)
- Tai-Danae Bradley (blog)
- Azimuth Project - (blog)
- The n-Category Cafe (blog)
- PL Perspectives - SIGPLAN (blog)
- Stack project online book ~7k pages about algebraic geometry:
Part 1: Preliminaries covers category theory (including sheaves, sites, simplical sets, fibrations), algebra, topology, cohomology
Part 2: Schemes
Part 3: Topics in Scheme Theory
Part 4: Algebraic Spaces
Part 5: Topics in Geometry
Part 6: Deformation Theory
Part 7: Algebraic Stacks
Part 8: Topics in Moduli Theory - Quantum Gravity Seminar - John Baez interesting notes around type theory (in classical versus quantum computation) and (cohomology and computation)
- Fancy Algebra - Part I: Adjoint Functors
- varkor/quiverTooll for drawing commuate diagrams
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
- Samson Abramsky
- Benedikt Ahrens, personal page
- Thorsten Altenkirch, University of Nottingham page
- Nada Amin, Cambridge University page
- Carlo Angiuli, Carnegie Mellon University page, arxiv
- Robert Atkey
- John Baez, University of California page
- Michael Barr
- Edwin Brady, personal page
- Olivia Caramello, 1, 2, 3
- Eugenia Cheng
- J. R. B. Cockett
- Thierry Coquand
- Brian Day, arXiv
- Peter Dybjer, Chalmers University page
- Conal Elliott, personal page
- Martín Hötzel Escardó, University of Birmingham page
- Eric Finster, personal page
- Brendan Fong, [personal page](Brendan Fong)
- Murdoch James Gabbay, arxiv
- Fabrizio Genovese, arxiv
- Neil Ghani
- Jeremy Gibbons
- Robert Harper, Carnegie Mellon University
- Ralf Hinze
- John Hughes
- Graham Hutton, University of Nottingham page
- Valery Isaev, JET Brains Research page
- Mauro Jaskelioff
- Johan Jeuring, Utrecht University page
- André Joyal, arxiv
- Jacob Lurie
- Jade Master
- Lucius Gregory Meredith
- David Jaz Myers, arxiv
- Martin Odersky, EPFL page
- Craig A. Pastro, arXiv
- Simon Peyton Jones, MS Reasearch page
- Oleg Kiselyov, personal page
- Jacob Lurie
- Conor McBride
- Heather Miller
- Ulf Norell, University of Gothenburg page
- Russell O'Connor
- Emily Riehl
- Exequiel Rivas
- Peter Selinger, Dalhousie University page
- David Spivak, arXiv
- Jon Sterling
- Ross Street, wikipedia has links to publications, arXiv
- Wouter Swierstra, Utrecht University page
- Tarmo Uustalu, arXiv
- Christina Vasilakopoulou, arXiv
- Philip Wadler, Monads, arrows, applicatives, Parametricity
- 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
- State of formalization of mathematics in Lean (blog post)
- Archive of Formal Proofs in Isabelle
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)
- Computational Type Theory - OPLSS 2018 - Robert Harper (course), lecture notes, high quality videos, (video playlist) - lower quality videos
- Introduction to Univalent Foundations of Mathematics with Agda - MGS 2019 - Martín Hötzel Escardó (lecture notes) (github)
- 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)
- Introduction to Univalent Foundations of Mathematics with Agda - MGS 2019 - Martín Hötzel Escardó (lecture notes) (github)
- Cubical Agda and its extensions, HoTTEST - Andrea Vezzosi (code), (video)
- Cubical Tutorial. Introduction Course - Maxim Sokhatsky plan and notes of seminar about HoTT and Cubical TT, moreMaxim Sokhatsky plan and notes of seminar about HoTT and Cubical TT, more
- 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
- CT formulated in terms of UF/HoTT nLab
- Category Theory in Idris statebox/idris-ct
- Category Theory in Haskell by Sjoerd Visscher data-category
- Category Theory and Topos Theory in Scala by Vlad Patryshev vpatryshev/Categories
- Monoidal categories in Python oxford-quantum-group/discopy, paper: DisCoPy: Monoidal Categories in Python Giovanni de Felice, Alexis Toumi, Bob Coecke arxiv 2005.02975
- Evan Patterson: Realizing Applied Category Theory in Julia (video)
- 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)
- Logical_Graphs
- Applied Logic course - Erik Palmgren (contains nice lecture notes, exercises in Coq)
- Equivariant ZFA and the foundations of nominal techniques - Murdoch J. Gabbay (arXiv:1801.09443)
- Overwiev Nominal Techniques - Andrew Pitts (pdf)
- 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)
- SPLV 2020 - Maribel Fernandez - Nominal rewriting and unification, Jamie Gabbay - Nominal datatypes
- Constructive Representation of Nominal Sets in Agda - Pritam Choudhury (pdf)
- Libraries:
- ekmett/name, live coding: Haskell Live-Coding, Session 18 (video)
- selinger/nominal
- bellissimogiorno/nominal presented at SPLV 2020(video playlist)
- AlphaProlog
- AlphaKanren
- http://petrinet.org/
- Topics in Concurrency - Cambridge 2018–19 Course materials
- Higher Algebra - Jacob Lurie (pdf)
- Algebraic Operads - Jean-Louis Loday and Bruno Vallette (pdf v 0.99)
- Foundations of Algebraic Theories and Higher Dimensional Categories - Soichiro Fujii (arxiv:1903.07030)
- A unified framework for notions of algebraic theory - Soichiro Fujii (paper)
- 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
- Evan Patterson Wiki Logic and PLT, Algebra and Category Theory, Sheafs, cubical, simplical stuff
- 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
- Haskell from Scratch - Chris Forno @jekor (video playlist)
Haskell user groups, commmunities videos
- Boston Haskell
- Haskell at Work
- NYC Haskell User's Group
- Monadic Warsaw
- LambdaConf
- London Haskell
- FPComplete videos
- FooCafe - videos Haskell
- GoogleTechTalks - Haskell
- Microsoft Research - Haskell
- Functional Tricity