David Richter retweetledi
📄 A Direct-Style Effect Notation for Sequential and Parallel Programs by @drcicer, Timon Böhler, Pascal Weisenburger, and @m_mezini - arxiv.org/abs/2305.08496
Dansk
David Richter
30 posts
David Richter
@drcicer
❤️ programming languages. phd student at @stg_darmstadt. DR are my initials not my title.
Germany Katılım Eylül 2014
110 Takip Edilen26 Takipçiler
Filipino
Prisma is a multitier language for secure smart contracts. David presenting our work at @ECOOPconf #Ethereum #multitierprogramming @m_mezini @SebastFaust
English
@ProfMaxNew stuff, property, structure, thing, object, gadget, widget, container, category, ...
English
Half of PL research is coming up with new synonyms for "type" because you already made a formal definition for all the others: type, kind, sort, set, collection, class, ...
English
We also evaluate the performance of the compiler generated code to show that its similar to handwritten Solidity code. In contrast to other smart contract languages using linear, type-state or session types, Prisma is inspired by tierless and choreographic programming.
English
We formalise compilation&evaluation. Although compiler goes through heavy changes like CPS and defunctionalisation, we show that malicious client code 👿 cant distinguish contract code from before or after compilation (secure compilation), after inserting control-flow guards🛡️
English
Prisma is a language / Scala library for writing distributed programs that interact via efficient and safe Ethereum smart contracts. @drcicer, Kretzler, Weisenburger, @guidosalva, @SebastFaust, @m_mezini #ecoop22
➡2022.ecoop.org/details/ecoop-…
➡️arxiv.org/pdf/2205.07780…
Details below…
English
@guidosalva @realThesave @OrnelaDardha @fangyi_zhou_ @Simon_JF @drcicer @jacopo_mauro @marcoperessotti @carbonem
Fano, Marche 🇮🇹 QAM
Choreographic languages fam, make sure to check out @andrewkhirsch and Deepak Garg's distinguished POPL paper! Especially if you're into mechanised proofs (with @CoqLang in this case).
Andrew K. Hirsch@andrewkhirsch
I'm excited to announce that my POPL paper coming out in January won a distinguished paper award!
Fano, Marche 🇮🇹 English
@famontesi (Although its titled categorical logic, 95% of the pages contain only inference rules and no commutative diagrams 😅)
English
@famontesi The only book that contains inference rules and is called an introduction that i read recently is the following: mikeshulman.github.io/catlog/catlog.… :D
English
@schrijvers_tom Ah! Initially I thought algebraic < scoped < latent, and the expected the I to be the effect. But I suppose the paper actually says to separate the latent part of the effect from the non-latent part. I probably need to reread it. The video is also nice😀
English
@drcicer Nondeterminism is an algebraic effect. Algebraic effects are a special case where l is the identity functor.
Often l is a special kind of state, sometimes it has more structure (e.g., an applicative functor) where l () is not uncommon.
English
Join APLAS 2021 later today to see Birthe present our paper on Latent Effects. arxiv.org/abs/2108.11155
English
CPS translation gives every function another parameter (to be called with the result of the function) (\x.M := \x\k.M), and every application another argument (M N := M N K); and additionally all terms another argument to be called with the result of the term (... := \k.k ...).
English
Looking for nice equations. Today, continuation passing style translation: Via Griffin, POPL 1989. A formulae-as-type notion of control
English
Namely, the we must be able to pick a enclosing description (data) for any predicate (function), but we cant just try the function for all possible inputs to look for the best description (potentially infinite)! With a Kleisli GC, we return the element safely hidden in a monad.
English
Looks cool: Constructive Galois Connections, JFP'18, Darais, Horn. The problem is, how can we extract static analyses from mechanized soundness proofs for Galois Connections (GC)? The authors propose "Kleisli GC".
English
David Richter retweetledi
Since Manifest V3's "performance" argument is back in the current news cycle, a reminder of what "Understanding the Performance Costs and Benefits of Privacy-focused Browser Extensions" concluded: twitter.com/gorhill/status…
R. Hill@gorhill
"Understanding the Performance Costs and Benefits of Privacy-focused Browser Extensions": "we urge browser vendors to retain functionality necessary for privacy-focused extensions, but which is slated for deprecation, as the [...] performance argument does not appear to be valid"
English
David Richter retweetledi
The presentation of our @ECOOPconf distinguished paper on Multiparty Languages is online! 👀
youtu.be/zx07I-f7ZME
w/ @realThesave, @marcoperessotti, @drcicer, @guidosalva, and P. Weisenburger.
*Six* speakers in a 15 min 📽️!
Mini 🧵 on the paper in the 1st comment 👇.
YouTube
English
@rob_rix Cool! But why not apply id to extract?
Oh, I see! Only if r is existential not universal. 😃
{-# LANGUAGE RankNTypes, TypeApplications #-}
type CPS a b = forall r. (b -> r) -> (a -> r)
pure :: (a -> b) -> CPS a b
pure f g = g . f
extract :: CPS a b -> (a -> b)
extract k = k id
English
