JENSFEST 2024
who it's for
programming language researchers, compiler engineers, formal methods researchers, compiler backend engineers, programming language educators, software architects, verification engineers
topics
Coq-checked nested summation formulas; lifting CompCert proofs to multithreading; Virgil unboxed and packed ADTs; flyweight as language-level memoization; Agda verification of denotational inheritance; MiniJava targeting RISC-V with GC; Coccinelle program transformation tool; private set intersection attacks on BLS; normalization barrier and self-evaluators; determinism proofs for structured parallelism; proof-carrying analysis for Java optimizations
| title | author | length |
|---|---|---|
| Closing Remarks | Jens Palsberg | 19m |
Closing remarks list concrete habits, outcomes and a looming deadline: advice to make progress every day, judge work as new interesting difficult, use focused… | ||
| Nested Summations | Olivier Danvy | 16m |
This work claims explicit formulas that express Fibonacci, Lucas, Jacobstahl and Jacobstahl‑Lucas sequences as finitely nested finite sums, gives the… | ||
| Dennis's talk | Dennis Brylow | 20m |
Builds a statewide pipeline to staff K–12 CS: wins NSF funding, co‑chairs 2017 standards, creates the Wisconsin Dairyland CSTA chapter, and runs workshops that… | ||
| Stories of Jens Palsberg for Fun and Profit | V Krishna Nandivada | 12m |
A series of anecdotes centers on concrete results: a 50 sheep story about time reallocation, a provable fix for type-safe method inlining that explains why… | ||
| The Normalization Barrier Revisited | Shuo Ding, Qirun Zhang | 16m |
Revisits Brown and Palsberg’s POPL 2016 result and shows that if the interpreter embeds type checking and accepts untyped representations (Church numerals… | ||
| The Essence of the Flyweight Design Pattern | Fernando Magno Quintão Pereira, Caio Raposo | 25m |
Claims that the Flyweight pattern becomes a language feature by adding safe memoization of constructors, implements it in the Hush language (runtime in Rust)… | ||
| Jens, the Ultimate PL Renaissance man! | Vivek Sarkar | 19m |
A concise history of concrete results: a formal featherweight X10 language models structured parallelism with async and finish and proves a progress theorem… | ||
| Unboxing Virgil ADTs For Fun and Profit | Bradley Wei Jie Teo, Ben L. Titzer | 27m |
Adds two annotations to Virgil: #unboxed removes heap allocation by lowering non-nullary ADT cases into multiple machine scalars/words, and #packed lets the… | ||
| Correct Compilation of Concurrent C Code | John Bender | 23m |
Claims a way to lift CompCert’s single‑thread forward‑proofs to multithreaded C by parameterizing the single‑thread semantics with nondeterministic choices… | ||
| Towards Verification of a Denotational Semantics of Inheritance | Peter D. Mosses | 24m |
An Agda formalisation replicates the OOPSLA ’89 operational and denotational definitions of inheritance, uses Agda proof assistant to check the equivalence via… | ||
| MiniJava on RISC-V: A Game of Global Compilers Domination | Jack Forden, Alexander Gebhard, Maverick Berner, Dennis Brylow | 25m |
MiniJava compiles to real RISC-V boards by replacing Appel/Palsberg’s ARM-focused instruction selection and register allocation with RISC-V-specific code… | ||
| Lost and Found in the Fog of Trust | Özgür Kesim, Christian Grothoff | 16m |
Protocol promises private computation of the size of the intersection between Victor’s trusted keys and Peggy’s witnesses, but formalization finds two attacks… | ||
| Coccinelle: Program transformation in the real world | Julia Lawall | 21m |
Coccinelle provides a small semantic patch language that matches C source patterns using meta-variables and a ... operator to express general edits, then… | ||
| Welcome | Todd Millstein | 07m |
A short welcome recounts concrete ways Jens shapes careers: three roles — mentor, citizen, explorer — with specifics: coauthored the presenter's first grant… | ||
| nothing matches | ||