A Dependently Typed Calculus with Pattern Matching and Erasure Inference
https://dl.acm.org/doi/pdf/10.1145/3408973
https://dl.acm.org/doi/pdf/10.1145/3408973
👍1
The Unreasonable Effectiveness of Multiple Dispatch
https://www.juliaopt.org/meetings/santiago2019/slides/stefan_karpinski.pdf
https://www.juliaopt.org/meetings/santiago2019/slides/stefan_karpinski.pdf
👍2
When should you choose C++ as your starting language?
https://steelph0enix.github.io/posts/choosing-first-language
https://steelph0enix.github.io/posts/choosing-first-language
steelph0enix.github.io
When should you choose C++ as your starting language?
Short answer: probably never.
😎4👎2🤯1
Partial Computation of Programs
Yoshihiko Futamura
https://repository.kulib.kyoto-u.ac.jp/dspace/bitstream/2433/103401/1/0482-14.pdf
Yoshihiko Futamura
https://repository.kulib.kyoto-u.ac.jp/dspace/bitstream/2433/103401/1/0482-14.pdf
Supercompiler HOSC 1.0: under the hood
https://keldysh.ru/papers/2009/source/prep2009_63_eng.pdf
https://keldysh.ru/papers/2009/source/prep2009_63_eng.pdf
Efficient normalization by evaluation
https://inria.hal.science/inria-00434283/document
https://inria.hal.science/inria-00434283/document
Normalization by evaluation and algebraic effects
https://danel.ahman.ee/papers/mfps13.pdf
https://danel.ahman.ee/papers/mfps13.pdf
A context-based approach to proving termination of evaluation
https://ii.uni.wroc.pl/~mabi/papers/mfps09.pdf
https://ii.uni.wroc.pl/~mabi/papers/mfps09.pdf
👍1
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