Clowns to the Left of me, Jokers to the Right
http://strictlypositive.org/CJ.pdf
http://strictlypositive.org/CJ.pdf
Demystifying Differentiable Programming: Shift/Reset the Penultimate Backpropagator
https://arxiv.org/abs/1803.10228
[Thanks to Elias]
https://arxiv.org/abs/1803.10228
[Thanks to Elias]
Brouwer's fixed-point theorem in real-cohesive homotopy type theory
https://arxiv.org/abs/1509.07584
https://arxiv.org/abs/1509.07584
arXiv.org
Brouwer's fixed-point theorem in real-cohesive homotopy type theory
We combine Homotopy Type Theory with axiomatic cohesion, expressing the latter internally with a version of "adjoint logic" in which the discretization and codiscretization modalities are...
Internal Universes in Models of Homotopy Type Theory
https://arxiv.org/abs/1801.07664
https://arxiv.org/abs/1801.07664
Recovering Purity with Comonads and Capabilities
https://arxiv.org/pdf/1907.07283.pdf
https://arxiv.org/pdf/1907.07283.pdf
Surreal Ordered Exponential Fields
https://arxiv.org/pdf/2002.07739.pdf
https://arxiv.org/pdf/2002.07739.pdf
Non-distributive Logics: From Semantics to Meaning
https://arxiv.org/pdf/2002.04257.pdf
https://arxiv.org/pdf/2002.04257.pdf
Mathematical Structures
http://math.chapman.edu/~jipsen/structures/doku.php
An extremely comprehensive list.
http://math.chapman.edu/~jipsen/structures/doku.php
An extremely comprehensive list.
Polygroups Derived from Cogroups
https://core.ac.uk/download/pdf/82131375.pdf
https://core.ac.uk/download/pdf/82131375.pdf
Advanced Programming Languages: The Case for Haskell, Scala, SML/OCaml, and Scheme
http://matt.might.net/articles/best-programming-languages
http://matt.might.net/articles/best-programming-languages
Promonads, Arrows, and Einstein Notation for Profunctors
https://bartoszmilewski.com/2019/03/27/promonads-arrows-and-einstein-notation-for-profunctors/
https://bartoszmilewski.com/2019/03/27/promonads-arrows-and-einstein-notation-for-profunctors/
Functional Programming in OCaml
Spring 2020 Edition
https://www.cs.cornell.edu/courses/cs3110/2020sp/textbook/
Spring 2020 Edition
https://www.cs.cornell.edu/courses/cs3110/2020sp/textbook/
Miranda, the predecessor of Haskell, is now free software
https://www.cs.kent.ac.uk/people/staff/dat/miranda/
https://www.cs.kent.ac.uk/people/staff/dat/miranda/
www.cs.kent.ac.uk
Miranda homepage
The Miranda functional programming system homepage
Linear Logic for Constructive Mathematics
https://golem.ph.utexas.edu/category/2018/05/linear_logic_for_constructive.html
https://golem.ph.utexas.edu/category/2018/05/linear_logic_for_constructive.html
Named Typeclasses in Haskell
http://marcosh.github.io/post/2019/11/11/named-typeclasses-in-haskell.html
http://marcosh.github.io/post/2019/11/11/named-typeclasses-in-haskell.html
Marcoshplace
Named typeclasses in Haskell
Mathematical Components
https://math-comp.github.io/mcb/book.pdf
https://math-comp.github.io/mcb/book.pdf
Short Introduction to Enriched Categories
http://www-lmpa.univ-littoral.fr/~stubbe/PDF/EnrichedCatsKLUWER.pdf
http://www-lmpa.univ-littoral.fr/~stubbe/PDF/EnrichedCatsKLUWER.pdf
Basic Concepts of Enriched Category Theory
http://www.tac.mta.ca/tac/reprints/articles/10/tr10.pdf
http://www.tac.mta.ca/tac/reprints/articles/10/tr10.pdf
A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory
https://arxiv.org/pdf/1605.03227
https://arxiv.org/pdf/1605.03227
A Verified Implementation of Algebraic Numbers in Isabelle/HOL
https://link.springer.com/content/pdf/10.1007/s10817-018-09504-w.pdf
https://link.springer.com/content/pdf/10.1007/s10817-018-09504-w.pdf