Practical Foundations for Programming Languages (Second Edition): Bob Harper
https://www.cs.cmu.edu/~rwh/pfpl/
https://www.cs.cmu.edu/~rwh/pfpl/
The MMT Language and System
https://uniformal.github.io/
Imagine model theory, but you can choose the logic, the concept of homomorphism is internal to everything, there is a proof checker and a IDE.
This is close to being the hottest concept I ever saw.
https://uniformal.github.io/
Imagine model theory, but you can choose the logic, the concept of homomorphism is internal to everything, there is a proof checker and a IDE.
This is close to being the hottest concept I ever saw.
MultiMLton: A Multicore-Aware Runtime for Standard ML
https://cse.buffalo.edu/~lziarek/JFP_MultiMLton.pdf
https://cse.buffalo.edu/~lziarek/JFP_MultiMLton.pdf
On a Category of Cluster Algebras
https://arxiv.org/pdf/1201.5986.pdf
https://arxiv.org/pdf/1201.5986.pdf
Building Type Theories 1: Induction-Recursion
https://sofiafaro.wordpress.com/2019/11/06/building-type-theories-1/
https://sofiafaro.wordpress.com/2019/11/06/building-type-theories-1/
Sofia Faro
Building Type Theories 1: Induction-Recursion
I want to show you a technique for building a new type theory quickly. I use it to test and refine type theoretic ideas, without spending too much time. We’re going to build a small type theo…
Unix System Programming with Standard ML
http://mlton.org/References.attachments/Shipman02.pdf
Not exactly related to this channel, but probably useful for some viewing it
http://mlton.org/References.attachments/Shipman02.pdf
Not exactly related to this channel, but probably useful for some viewing it
John_H_Reppy_Concurrent_Programming.pdf
891 KB
Concurrent Programming in Standard ML (1999/2007)
Temporal Type Theory
https://arxiv.org/abs/1710.10258
https://arxiv.org/abs/1710.10258
arXiv.org
Temporal Type Theory: A topos-theoretic approach to systems and behavior
This book introduces a temporal type theory, the first of its kind as far as we know. It is based on a standard core, and as such it can be formalized in a proof assistant such as Coq or Lean by...
Optimizing Optimal Reduction: A Type Inference Algorithm for Elementary Affine Logic
http://www.cs.unibo.it/~martini/papers-to-ftp/EA-typing.pdf
[Thanks to Parra]
http://www.cs.unibo.it/~martini/papers-to-ftp/EA-typing.pdf
[Thanks to Parra]
Lambda-calculus and Combinatory Logic
https://www.lama.univ-savoie.fr/pagesmembres/david/ftp/hindley.pdf
https://www.lama.univ-savoie.fr/pagesmembres/david/ftp/hindley.pdf
ICALP 2020 (http://econcs.pku.edu.cn/icalp2020/) and LICS 2020 (https://lics.siglog.org/lics20/) will take place in co-location from 8th till 12th of July 2020 in Beijing, China. The conferences will be preceded by two days of joint workshops, held on July 6th and 7th. We invite proposals of workshops affiliated with ICALP-LICS 2020 on all topics covered by ICALP and LICS, as well as other areas of theoretical computer science.
econcs.pku.edu.cn
ICALP 2020-EconCS@PKU
The Convolution of Comonads is a Comonad
https://mathoverflow.net/questions/346529/the-convolution-of-comonads-is-a-comonad
(Thanks to
https://mathoverflow.net/questions/346529/the-convolution-of-comonads-is-a-comonad
(Thanks to
Fo Uche)MathOverflow
The convolution of comonads is a comonad
$\def\Cat{\mathbf{Cat}}\def\Set{\mathbf{Set}}\def\A{\mathcal{A}}$I stumbled into the following statement:
Let $\Cat(\Set,\Set)_s$ be the category of small functors[¹] $F : \Set \to\Set$ and let $F...
Let $\Cat(\Set,\Set)_s$ be the category of small functors[¹] $F : \Set \to\Set$ and let $F...