Features of a dream programming language: 3rd draft
https://magnemg.eu/features-of-a-dream-programming-language-3rd-draft
https://magnemg.eu/features-of-a-dream-programming-language-3rd-draft
Magne's blog
Features of a dream programming language: 3rd draft
Have you ever dreamt of what features your ideal programming language would have? Have you ever tried to make a list of the best features (or non-features) of existing languages that are particularly inspired in some way...?
This article explores and...
This article explores and...
The Boolean Satisfiability Problem: an overview of solving techniques and applications
https://inria.hal.science/hal-03589602/file/ClementinTayou-mai2021.pdf
https://inria.hal.science/hal-03589602/file/ClementinTayou-mai2021.pdf
Lone is a freestanding Lisp interpreter designed to run directly on top of the Linux kernel with full support for Linux system calls. It has zero dependencies, not even the C standard library.
https://github.com/lone-lang/lone
https://github.com/lone-lang/lone
GitHub
GitHub - lone-lang/lone: The standalone Linux Lisp
The standalone Linux Lisp. Contribute to lone-lang/lone development by creating an account on GitHub.
๐ฑ3โค2๐ฅ2
Programming and Reasoning with Algebraic Effects and Dependent Types
Edwin C. Brady
https://www.type-driven.org.uk/edwinb/papers/effects.pdf
Edwin C. Brady
https://www.type-driven.org.uk/edwinb/papers/effects.pdf
๐2
The algebra of boolean satisfiability
https://piedeleu.com/posts/algebra-of-sat/
https://piedeleu.com/posts/algebra-of-sat/
๐3
Higher-Kinded Data
https://reasonablypolymorphic.com/blog/higher-kinded-data/
https://reasonablypolymorphic.com/blog/higher-kinded-data/
Arend is a theorem prover and a programming language based on Homotopy Type Theory.
https://github.com/JetBrains/Arend
https://github.com/JetBrains/Arend
GitHub
GitHub - JetBrains/Arend: The Arend Proof Assistant
The Arend Proof Assistant. Contribute to JetBrains/Arend development by creating an account on GitHub.
๐1
Introduction to the Calculus of Inductive Constructions
https://inria.hal.science/hal-01094195/document
https://inria.hal.science/hal-01094195/document
๐1
Handlers in Action
https://homepages.inf.ed.ac.uk/slindley/papers/handlers.pdf
https://homepages.inf.ed.ac.uk/slindley/papers/handlers.pdf
Contracts for Higher-Order Functions
https://users.cs.northwestern.edu/~robby/pubs/papers/ho-contracts-icfp2002.pdf
https://users.cs.northwestern.edu/~robby/pubs/papers/ho-contracts-icfp2002.pdf
๐1
Elaboration with First-Class Implicit Function Types
https://dl.acm.org/doi/pdf/10.1145/3408983
https://dl.acm.org/doi/pdf/10.1145/3408983
๐1
Donโt Substitute Into Abstractions (Functional Pearl)
https://benl.ouroborus.net/papers/2016-dsim/lambda-dsim-20160328.pdf
https://benl.ouroborus.net/papers/2016-dsim/lambda-dsim-20160328.pdf
Continuous Normalization for the Lambda-Calculus and Gรถdelโs T
https://citeseerx.ist.psu.edu/document?repid=rep1&type=pdf&doi=b42488e06239b71c12d429db1895063e25601e8b
https://citeseerx.ist.psu.edu/document?repid=rep1&type=pdf&doi=b42488e06239b71c12d429db1895063e25601e8b
๐1๐1