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
Tailored Termination for Optimal Supercompilation
https://www.cs.purdue.edu/homes/bendy/TailoredSuperOptimization/BespokeSO.pdf
https://www.cs.purdue.edu/homes/bendy/TailoredSuperOptimization/BespokeSO.pdf
π€2
Why I Use the GPL and Not Cuck Licenses
https://lukesmith.xyz/articles/why-i-use-the-gpl-and-not-cuck-licenses/
https://lukesmith.xyz/articles/why-i-use-the-gpl-and-not-cuck-licenses/
lukesmith.xyz
Why I Use the GPL and Not Cuck Licenses | Luke Smith
Undermining the copyright system is seriously important and copyleft licenese do the needful.
π₯4π2π€2π1
ITT-Flavored Calculus of Constructions Type Checker
https://gist.github.com/VictorTaelin/dd291148ee59376873374aab0fd3dd78
https://gist.github.com/VictorTaelin/dd291148ee59376873374aab0fd3dd78
Gist
ITT-Flavored Calculus of Constructions Type Checker
ITT-Flavored Calculus of Constructions Type Checker - itt-coc.ts
π€―1
Time- and Size-Efficient Supercompilation
https://www.diva-portal.org/smash/get/diva2:999818/FULLTEXT01.pdf
https://www.diva-portal.org/smash/get/diva2:999818/FULLTEXT01.pdf
β€4
A Self-Applicable Supercompiler
https://refal.botik.ru/library/Nemytykh-Pinchuk-Turchin_A_Self-Applicable_Supercompiler_(LNCS_vol_1110,_1996,_pp_322-337).pdf
https://refal.botik.ru/library/Nemytykh-Pinchuk-Turchin_A_Self-Applicable_Supercompiler_(LNCS_vol_1110,_1996,_pp_322-337).pdf
β€1π±1
Why is Idris 2 so much faster than Idris 1?
https://www.type-driven.org.uk/edwinb/category/posts.html
https://www.type-driven.org.uk/edwinb/category/posts.html
www.type-driven.org.uk
Edwin Brady Posts
β€2
Typelevel Brainfuck in Haskell; Brainfuck implemented solely in Haskell's type system
https://github.com/toptobes/typefuck-haskell
https://github.com/toptobes/typefuck-haskell
GitHub
GitHub - toptobes/typefuck-haskell: Typelevel Brainfuck; Brainfuck implemented solely in Haskell's type system (no TemplateHaskell)
Typelevel Brainfuck; Brainfuck implemented solely in Haskell's type system (no TemplateHaskell) - GitHub - toptobes/typefuck-haskell: Typelevel Brainfuck; Brainfuck implemented solely in Ha...
β€2
A tutorial implementation of dynamic pattern unification
https://adam.gundry.co.uk/pub/pattern-unify/pattern-unification-2012-07-10.pdf
https://adam.gundry.co.uk/pub/pattern-unify/pattern-unification-2012-07-10.pdf
π₯1
Convergence of program transformers in the metric space of trees
https://www.sciencedirect.com/science/article/pii/S016764239900026X
https://www.sciencedirect.com/science/article/pii/S016764239900026X
π€1
Metavariables: their Implementation and Use in Program Transformation
https://pat.keldysh.ru/~roman/doc/Turchin/1995-Turchin_Nemytykh--Metavariables_their_Implementation_and_Use_in_Program_Transformation.pdf
https://pat.keldysh.ru/~roman/doc/Turchin/1995-Turchin_Nemytykh--Metavariables_their_Implementation_and_Use_in_Program_Transformation.pdf
π1π₯1
Solving SAT via interaction net superpositions
https://gist.github.com/VictorTaelin/9061306220929f04e7e6980f23ade615
https://gist.github.com/VictorTaelin/9061306220929f04e7e6980f23ade615
Gist
Simple SAT Solver via superpositions
Simple SAT Solver via superpositions. GitHub Gist: instantly share code, notes, and snippets.
π₯1π€1