Category Theory with Bartosz Milewski: podcast
https://corecursive.com/035-bartosz-milewski-category-theory/
https://corecursive.com/035-bartosz-milewski-category-theory/
CoRecursive Podcast
Category Theory - CoRecursive Podcast
Today Adam talks to Bartosz Milewski. He is the author of a popular blog series, lecture series, and now book on Category Theory for programmers.The world of functional programming is rife with terminology imported from abstract algebra and Category Theory.…
The Type Theory Podcast
http://typetheorypodcast.com/
http://typetheorypodcast.com/
Homotopy Patch Theory
http://dlicata.web.wesleyan.edu/pubs/amlh14patch/amlh14patch.pdf
http://dlicata.web.wesleyan.edu/pubs/amlh14patch/amlh14patch.pdf
Kerodon - an online resource for homotopy-coherent mathematics
https://kerodon.net/kerodon.pdf
WIP book, requires basic knowledge of topology.
[Thanks to H]
https://kerodon.net/kerodon.pdf
WIP book, requires basic knowledge of topology.
[Thanks to H]
Forwarded from Cab
Also, a little disclamer. We have small meetings each Wednesday evening, chatting about category theory, Coq, ssreflect, HoTT, FP in general, NixOS — and all that good stuff. We are gathering in Kocherga (Moscow).
If you want to participate — PM me) (usually comes from 4 to 6 people)
If you want to participate — PM me) (usually comes from 4 to 6 people)
The Five Stages of Accepting Constructive Mathematics: Andrej Bauer
https://www.youtube.com/watch?v=21qPOReu4FI
https://www.youtube.com/watch?v=21qPOReu4FI
YouTube
Five Stages of Accepting Constructive Mathematics - Andrej Bauer
Andrej Bauer
University of Ljubljana, Slovenia; Member, School of Mathematics
March 18, 2013
Discussions about constructive mathematics are usually derailed by philosophical opinions and meta-mathematics. But how does it actually feel to do constructive mathematics?…
University of Ljubljana, Slovenia; Member, School of Mathematics
March 18, 2013
Discussions about constructive mathematics are usually derailed by philosophical opinions and meta-mathematics. But how does it actually feel to do constructive mathematics?…
1029786.1029818.pdf
644.2 KB
Logicians who reason about themselves
[Thanks to (a)]
[Thanks to (a)]
Forwarded from HH
Pointwise Kan extensions
I'm going to post again one of Bartosz's ingeniously simple written articles on category theory, this time it will be an introduction to pointwise Kan extensions. Although MacLane covers nearly everything you need to know about pointwise Kan extensions I think there's a huge benefit from approaching it from a slighty different angle, also Bartosz provides a Haskell implementation of Kan extensions (Kmetts library) in the end so programmers might also want to look into it.
https://bartoszmilewski.com/2018/01/23/pointwise-kan-extensions/
I'm going to post again one of Bartosz's ingeniously simple written articles on category theory, this time it will be an introduction to pointwise Kan extensions. Although MacLane covers nearly everything you need to know about pointwise Kan extensions I think there's a huge benefit from approaching it from a slighty different angle, also Bartosz provides a Haskell implementation of Kan extensions (Kmetts library) in the end so programmers might also want to look into it.
https://bartoszmilewski.com/2018/01/23/pointwise-kan-extensions/
Bartosz Milewski's Programming Cafe
Pointwise Kan Extensions
In my category theory blog posts, I stated many theorems, but I didn’t provide many proofs. In most cases, it’s enough to know that the proof exists. We trust mathematicians to do their…
Category Theory for Computing Science
http://www.tac.mta.ca/tac/reprints/articles/22/tr22.pdf
http://www.tac.mta.ca/tac/reprints/articles/22/tr22.pdf
seL4: Formal Verification of an OS Kernel
https://ts.data61.csiro.au/publications/nicta_full_text/1852.pdf
https://ts.data61.csiro.au/publications/nicta_full_text/1852.pdf
Linear Logic for Constructive Mathematics
https://arxiv.org/abs/1805.07518
https://arxiv.org/abs/1805.07518
arXiv.org
Affine logic for constructive mathematics
We show that numerous distinctive concepts of constructive mathematics arise automatically from an "antithesis" translation of affine logic into intuitionistic logic via a Chu/Dialectica...
Would aliens understand lambda calculus?
http://tomasp.net/blog/2018/alien-lambda-calculus/
[Thanks to Charlie Brown]
http://tomasp.net/blog/2018/alien-lambda-calculus/
[Thanks to Charlie Brown]
tomasp.net
Would aliens understand lambda calculus?
The question whether aliens would understand lambda calculus
is intriguing because it vividly formulates a fundamental question about our formal mathematical
knowledge. Are mathematical theories and results about them invented, i.e. constructed by
humans…
is intriguing because it vividly formulates a fundamental question about our formal mathematical
knowledge. Are mathematical theories and results about them invented, i.e. constructed by
humans…
Rewriting Type Theory
https://jesper.sikanda.be/posts/rewriting-type-theory.html
https://jesper.sikanda.be/posts/rewriting-type-theory.html
Formalizing ARM's Architecture Specification Language
https://alastairreid.github.io/specification_languages/
https://alastairreid.github.io/specification_languages/
alastairreid.github.io
ARM's Architecture Specification Language
What language should you write a specification in? Should you use the language
supported by your favourite verification tool (HOL, Verilog, …)?
Or should you write it in a DSL and translate that to whatever your
verification tool needs?
supported by your favourite verification tool (HOL, Verilog, …)?
Or should you write it in a DSL and translate that to whatever your
verification tool needs?
Reposting those introductory resources... Definitely worth taking a look at at least some of them
Forwarded from Pure & constructive mathematics in theory and use
[MLTT resources]
The original notes: https://archive-pml.github.io/martin-lof/pdfs/Bibliopolis-Book-retypeset-1984.pdf
A formal overview: https://ncatlab.org/nlab/show/Martin-L%C3%B6f+dependent+type+theory
Another denoscription: http://www.cse.chalmers.se/~peterd/papers/IntuitionisticTypeTheory150505.pdf
Programming in Martin-Löf type theory: https://www.dimap.ufrn.br/~regivan/pub/Programming_In_Martin_Loef_Type_Theory.pdf
[Resources for MLTT or similar about specific languages:]
Logic and Proof in Lean: https://leanprover.github.io/logic_and_proof/
General Theorem Proving in Lean: https://leanprover.github.io/theorem_proving_in_lean/
Programming Language Foundations in Agda: https://plfa.github.io/
Software foundations (based on Coq): https://softwarefoundations.cis.upenn.edu/current/index.html
The Nuprl Proof Development System: http://www.nuprl.org/book/
[HoTT resources]
The HoTT Book: https://homotopytypetheory.org/book/
HoTT in Agda: https://github.com/HoTT/HoTT-Agda
HoTT in Coq: https://github.com/HoTT/HoTT
The CoqHoTT project: http://coqhott.gforge.inria.fr/
Cubical type theory: https://arxiv.org/abs/1611.02108
Cubical type theory as Agda extension: https://agda.readthedocs.io/en/latest/language/cubical.html
Cubical Agda library: https://github.com/agda/cubical
The main implementation: https://github.com/mortberg/cubicaltt
An introduction to cubicaltt: https://homotopytypetheory.org/2017/09/16/a-hands-on-introduction-to-cubicaltt/
The original notes: https://archive-pml.github.io/martin-lof/pdfs/Bibliopolis-Book-retypeset-1984.pdf
A formal overview: https://ncatlab.org/nlab/show/Martin-L%C3%B6f+dependent+type+theory
Another denoscription: http://www.cse.chalmers.se/~peterd/papers/IntuitionisticTypeTheory150505.pdf
Programming in Martin-Löf type theory: https://www.dimap.ufrn.br/~regivan/pub/Programming_In_Martin_Loef_Type_Theory.pdf
[Resources for MLTT or similar about specific languages:]
Logic and Proof in Lean: https://leanprover.github.io/logic_and_proof/
General Theorem Proving in Lean: https://leanprover.github.io/theorem_proving_in_lean/
Programming Language Foundations in Agda: https://plfa.github.io/
Software foundations (based on Coq): https://softwarefoundations.cis.upenn.edu/current/index.html
The Nuprl Proof Development System: http://www.nuprl.org/book/
[HoTT resources]
The HoTT Book: https://homotopytypetheory.org/book/
HoTT in Agda: https://github.com/HoTT/HoTT-Agda
HoTT in Coq: https://github.com/HoTT/HoTT
The CoqHoTT project: http://coqhott.gforge.inria.fr/
Cubical type theory: https://arxiv.org/abs/1611.02108
Cubical type theory as Agda extension: https://agda.readthedocs.io/en/latest/language/cubical.html
Cubical Agda library: https://github.com/agda/cubical
The main implementation: https://github.com/mortberg/cubicaltt
An introduction to cubicaltt: https://homotopytypetheory.org/2017/09/16/a-hands-on-introduction-to-cubicaltt/
A Categorical Theory of Patches
https://www.youtube.com/watch?v=SnRFGZYo-xI
https://www.youtube.com/watch?v=SnRFGZYo-xI
YouTube
A Categorical Theory of Patches
When working with distant collaborators on the same documents, one often uses a version control system, which is a program tracking the history of files and helping importing modifications brought by others as patches. The implementation of such a system…