Lef

647 posts

Lef banner
Lef

Lef

@elefthei

Proofs @Rise_MSR, @MSFTResearch. Compilers, Formal Verification, Cryptography. Previous: @Penn, @Bridgewater, @MIT.

Seattle, WA เข้าร่วม Ağustos 2009
1.2K กำลังติดตาม1.2K ผู้ติดตาม
ทวีตที่ปักหมุด
Lef
Lef@elefthei·
🎉 Our paper “Structural Temporal Logic for Mechanized Program Verification” was accepted at OOPSLA 2025! We introduce Ticl, a program logic for compositional temporal proofs, beyond partial correctness, and directly over program syntax. #OOPSLA #Ticl 📄 arxiv.org/abs/2410.14906
English
2
8
63
3.7K
Lef
Lef@elefthei·
@hackerdocc If it’s wrong why does it feel so right
English
0
0
2
101
Eduardo
Eduardo@hackerdocc·
it's always "formal verification is pointless cuz the {spec, type-checker} can be wrong" but never "coding is pointless cuz the {code, tests} can be wrong" or "type-systems are pointless cuz the {types, type-checker} can be wrong"
English
8
2
54
6.3K
Lef รีทวีตแล้ว
Han Wang
Han Wang@handotdev·
how it feels listening to this podcast
Han Wang tweet media
Lisan al Gaib@scaling01

Andrej Karpathy calls AI Agents slop "Overall, the models they are not there. And I feel like the industry [...] it's making too big of a jump and it's trying to pretend that this is amazing. And it's not—it's slop! And I think they are not coming to terms with it. And maybe they are trying to fundraise or something like that, I'm not sure what's going on."

English
36
89
4.7K
846.7K
Lef
Lef@elefthei·
Thanks to everyone who came to my talk on #Ticl a “Structural Temporal Logic for Mechanized Program Verification” at #OOPSLA. Despite being in the last day, we had a pretty good turn out!
Lef tweet media
English
1
0
12
661
Lef
Lef@elefthei·
From Wawa to WA.
Filipino
0
0
8
169
Lef รีทวีตแล้ว
Alexander Hicks
Alexander Hicks@alexanderlhicks·
I'm hiring at the EF: jobs.lever.co/ethereumfounda… If you're into Ethereum, cryptography, and formal verification, please get in touch! 🙂
English
9
43
257
25.8K
Lef รีทวีตแล้ว
CAV
CAV@confCAV·
Emina Torlak from @AWS delivered a wonderful keynote about the Cedar authorization engine. #cav2025
CAV tweet media
English
0
1
12
608
Lef
Lef@elefthei·
@lastland0 We can definitely schedule this for next fall. I always enjoy visiting Portland.
English
0
0
1
37
Lef
Lef@elefthei·
🎓 I have successfully defended my PhD. Deeply thankful to my advisors Sebastian Angel and Steve Zdancewic for their support and mentorship throughout this journey. Next I’m joining Microsoft Research and the RiSE group to work on AI assisted verification.
Lef tweet media
English
13
5
138
8.2K
Lef รีทวีตแล้ว
joomy
joomy@joomy·
excited that my team at @Bloomberg is supporting PhD students in certified programming (and other infra/sec topics too!) through a fellowship. 💻🛡️ includes stipend, tuition, and internship. timely for Rocq and proof assistant folks as science funding tightens. please apply! 📬
Tech At Bloomberg@TechAtBloomberg

#CFP: Applications for Bloomberg’s 2025-2026 #Infrastructure & #Security Ph.D. #Fellowship are now being accepted. Submission Deadline: Friday, July 18, 2025 (11:59 PM AoE) bloom.bg/3HLdfmO #InfoSec #supplychainsecurity #ProgramAnalysis #BugFinding

English
0
4
41
3.4K
Lef
Lef@elefthei·
Reading in the editor is not the same as reading in the rendered PDF.
English
0
0
1
211
Lef
Lef@elefthei·
Theory is saying a DAG does not have cycles. Engineering is still adding a “visited” vector to the worklist algorithm because you know you will eventually hit a bug and it’s gonna be a pain to debug an infinite loop.
English
2
0
3
441
Lef
Lef@elefthei·
People using SMT solvers don’t know you can simply implement algebraic simplifications with smart constructors in 5x the time.
English
0
0
2
212
Lef
Lef@elefthei·
@MarisaVeryMoe Yes that is precisely what I was looking for! So staging an interpreter is good, but hard work. And the performance is still not as good as writing a compiler. I am using Rust so I will need quite a few tricks^TM to make this work. I am undecided but leaning don’t do it.
English
1
0
1
71
Lef
Lef@elefthei·
An interpreter is simply dynamic dispatch on a loop. A compiler trades dynamic dispatch for static dispatch. Can we have the cake (an interpreter) and eat it too (static dispatch)?
English
2
0
3
499
Lef
Lef@elefthei·
@MarisaVeryMoe Good idea! I imagine by using a language with partial evaluation you can get quite quite a bit of pattern matching done before getting the env. Then you are essentially dispatching only on references. Are you saying that practically the benefits are not that great?
English
1
0
1
40
Marisa "Long Middle Name Looks Cool" Kirisame
Marisa "Long Middle Name Looks Cool" Kirisame@MarisaVeryMoe·
@elefthei With staging you can get compiler in the form of a staged definitional interpreter, which is a somewhat useful trick to reduce complexity (or to increase performance, depending on which way you look). A light-weight form of this is to have interp : term -> env -> value (...)
English
2
0
1
115
Lef
Lef@elefthei·
@aaroneline Idk I always saw this style in old ML papers
English
1
0
0
28
Lef
Lef@elefthei·
I used to think ASTs with just two constructors UnaryOp and BinOp where old fashioned, but I think it actually saves a ton of lines of code (especially if using copilot).
English
2
0
0
261

ค้นพบ

@hackerdocc @AWS @lastland0 @Bloomberg @MarisaVeryMoe @elonmusk @BarackObama @taylorswift13