How to (re)invent Tait's Method, by Bob Harper
http://www.cs.cmu.edu/~rwh/pfpl/supplements/tait.pdf
http://www.cs.cmu.edu/~rwh/pfpl/supplements/tait.pdf
Theorems for free! by Philip Wadler
https://people.mpi-sws.org/~dreyer/tor/papers/wadler.pdf
https://people.mpi-sws.org/~dreyer/tor/papers/wadler.pdf
The Mathematical Specification of the Statebox language:
https://arxiv.org/abs/1906.07629
https://arxiv.org/abs/1906.07629
arXiv.org
The Mathematical Specification of the Statebox Language
This document defines the mathematical backbone of the Statebox programming language. In the simplest way possible, Statebox can be seen as a clever way to tie together different theoretical...
The Essence of Petri Net Gluings:
https://arxiv.org/abs/1909.03518
https://arxiv.org/abs/1909.03518
arXiv.org
The Essence of Petri Net Gluings
Many categorical frameworks have been proposed to formalize the idea of gluing Petri nets with each other. Such frameworks model net gluings in terms of sharing of resources or synchronization of...
Profunctor Optics: Modular Data Accessors:
https://arxiv.org/abs/1703.10857
https://arxiv.org/abs/1703.10857
arXiv.org
Profunctor Optics: Modular Data Accessors
CONTEXT: Data accessors allow one to read and write components of a data structure, such as the fields of a record, the variants of a union, or the elements of a container. These data accessors...
Chemoinformatics and structural bioinformatics in OCaml
https://jcheminf.biomedcentral.com/articles/10.1186/s13321-019-0332-0
https://jcheminf.biomedcentral.com/articles/10.1186/s13321-019-0332-0
BioMed Central
Chemoinformatics and structural bioinformatics in OCaml - Journal of Cheminformatics
Background OCaml is a functional programming language with strong static types, Hindley–Milner type inference and garbage collection. In this article, we share our experience in prototyping chemoinformatics and structural bioinformatics software in OCaml.…
What follows is a series of wonderful blog posts highlighting the transition of a well-established project from Python to OCaml. I hope it is useful for some of you to consider doing the same, or maybe choosing OCaml/SML or any ML for your next project!
Replacing Python: Candidates
http://roscidus.com/blog/blog/2013/06/09/choosing-a-python-replacement-for-0install/
Replacing Python: Second Round
http://roscidus.com/blog/blog/2013/06/20/replacing-python-round-2/
OCaml Binary Compatibility
http://roscidus.com/blog/blog/2013/07/07/ocaml-binary-compatibility/
Option Handling with OCaml Polymorphic Variants
http://roscidus.com/blog/blog/2013/08/31/option-handling-with-ocaml-polymorphic-variants/
Experiences with OCaml Objects
http://roscidus.com/blog/blog/2013/09/28/ocaml-objects/
OCaml Tips
http://roscidus.com/blog/blog/2013/10/13/ocaml-tips/
Asynchronous Python vs OCaml
http://roscidus.com/blog/blog/2013/11/28/asynchronous-python-vs-ocaml/
Polymorphism for Beginners
http://roscidus.com/blog/blog/2013/12/20/polymorphism-for-beginners/
OCaml: The Bugs So Far
http://roscidus.com/blog/blog/2014/01/07/ocaml-the-bugs-so-far/
OCaml: What You Gain
http://roscidus.com/blog/blog/2014/02/13/ocaml-what-you-gain/
Python to OCaml: Retrospective
http://roscidus.com/blog/blog/2014/06/06/python-to-ocaml-retrospective/
Replacing Python: Candidates
http://roscidus.com/blog/blog/2013/06/09/choosing-a-python-replacement-for-0install/
Replacing Python: Second Round
http://roscidus.com/blog/blog/2013/06/20/replacing-python-round-2/
OCaml Binary Compatibility
http://roscidus.com/blog/blog/2013/07/07/ocaml-binary-compatibility/
Option Handling with OCaml Polymorphic Variants
http://roscidus.com/blog/blog/2013/08/31/option-handling-with-ocaml-polymorphic-variants/
Experiences with OCaml Objects
http://roscidus.com/blog/blog/2013/09/28/ocaml-objects/
OCaml Tips
http://roscidus.com/blog/blog/2013/10/13/ocaml-tips/
Asynchronous Python vs OCaml
http://roscidus.com/blog/blog/2013/11/28/asynchronous-python-vs-ocaml/
Polymorphism for Beginners
http://roscidus.com/blog/blog/2013/12/20/polymorphism-for-beginners/
OCaml: The Bugs So Far
http://roscidus.com/blog/blog/2014/01/07/ocaml-the-bugs-so-far/
OCaml: What You Gain
http://roscidus.com/blog/blog/2014/02/13/ocaml-what-you-gain/
Python to OCaml: Retrospective
http://roscidus.com/blog/blog/2014/06/06/python-to-ocaml-retrospective/
miniKanren in Coq
https://github.com/dboulytchev/miniKanren-coq
https://github.com/dboulytchev/miniKanren-coq
Two mini/microKanrens in OCaml
https://github.com/JetBrains-Research/OCanren
https://github.com/StrykerKKD/Logical
https://github.com/JetBrains-Research/OCanren
https://github.com/StrykerKKD/Logical
Some HoTT Seminar whose page might be currently down depending on where you live
http://math.lsa.umich.edu/~simoncho/mwhottseminar.html
http://math.lsa.umich.edu/~simoncho/mwhottseminar.html
Forwarded from GNU Propaganda (Archived)
Which of these programming languages do you wish you could learn the most?
Anonymous Poll
18%
Common Lisp
11%
Scheme / Racket
8%
OCaml
2%
Mercury
3%
Prolog
9%
Scala
4%
Coq
39%
Haskell
5%
Idris
2%
Agda
Same question, but based on data only gained here
Anonymous Poll
15%
Common Lisp
7%
Scheme / Racket
9%
(OCa)ML
3%
Mercury
5%
Prolog
2%
Scala
6%
Coq
32%
Haskell
14%
Idris
6%
Agda
Note that I'll try to do a spotlight on the language most and the language least voted for, perhaps some blog post
Haskell might be excluded because it's way too easy to find tons of material about it, Idris is more interesting
Arend, a theorem prover based on HoTT
https://arend-lang.github.io
https://arend-lang.github.io
pi-base, a database of topological spaces
https://topology.jdabbs.com/
https://topology.jdabbs.com/
π-Base
A community database of topological theorems and spaces, with powerful search and automated proof deduction.