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
Bidirectional Elaboration of Dependently Typed Programs
https://www.cs.mcgill.ca/~fferre8/papers/BidirectionalElaboration.pdf
https://www.cs.mcgill.ca/~fferre8/papers/BidirectionalElaboration.pdf
๐ญ2๐1
Progress towards a GCC-based Rust compiler
https://lwn.net/SubscriberLink/954787/41470c731eda02a4/
https://lwn.net/SubscriberLink/954787/41470c731eda02a4/
lwn.net
Progress toward a GCC-based Rust compiler
The gccrs project is an ambitious
effort started in 2014 to implement a Rust compiler within The GNU Compiler
Collection (GCC). Even though the task is far from complete, progress has
been made since LWN's previous coverage,
according to reports from theโฆ
effort started in 2014 to implement a Rust compiler within The GNU Compiler
Collection (GCC). Even though the task is far from complete, progress has
been made since LWN's previous coverage,
according to reports from theโฆ
๐3๐1
A Roadmap to Metacomputation by Supercompilation
https://web.archive.org/web/20130628231908/https://repository.readscheme.org/ftp/papers/dagstuhl-pe96/02.pdf
https://web.archive.org/web/20130628231908/https://repository.readscheme.org/ftp/papers/dagstuhl-pe96/02.pdf
๐1
Transaction Isolation in Postgres DataBase
https://www.thenile.dev/blog/transaction-isolation-postgres
https://www.thenile.dev/blog/transaction-isolation-postgres
www.thenile.dev
Transaction Isolation in Postgres, explained
Ever dealt with glitches in a SaaS platform where your actions don't seem to sync up? That's often a transaction isolation issue in databases. Lets talk about transaction isolation and how they work in Postgres, so you can write reliable and performant codeโฆ
๐1
Handbook of Applied Cryptography
https://cacr.uwaterloo.ca/hac/
https://cacr.uwaterloo.ca/hac/
cacr.uwaterloo.ca
Handbook of Applied Cryptography
This site provides order information,
updates, errata, supplementary information, chapter bibliographies,
and other information for the Handbook of Applied
Cryptography by Menezes, van Oorschot and Vanstone.
updates, errata, supplementary information, chapter bibliographies,
and other information for the Handbook of Applied
Cryptography by Menezes, van Oorschot and Vanstone.
๐1