Stephanie Weirich
fancytypes.bsky.social
Stephanie Weirich
@fancytypes.bsky.social
Tell me about types
Reposted by Stephanie Weirich
OlivierFest’25 is taking place on October 14-15 at ICFP/SPLASH'25 in Singapore!

A two-day celebration of Olivier Danvy's impact on PL research, with a program packed with talks on algebraic effects, semantics, interpreters, and, of course, continuations.

conf.researchr.org/home/icfp-sp...
OlivierFest 2025 - ICFP/SPLASH 2025
This two-day event celebrates the career and accomplishments of Olivier Danvy on the occasion of his 64th birthday. Olivier is a visionary in the field of programming languages and is well-known for h...
conf.researchr.org
September 14, 2025 at 6:24 AM
Reposted by Stephanie Weirich
The United States has had a tremendous advantage in science and technology because it has been the consensus gathering point: the best students worldwide want to study and work in the US because that is where the best students are studying and working. 1/
May 31, 2025 at 1:21 PM
Reposted by Stephanie Weirich
1/3 The US didn’t end up leading the world in computing by luck. It happened because it made long-term, public investments in basic research, especially through NSF. That’s what created the breakthroughs that today’s tech companies are built on.
Isil Dillig on X: "1/3 The US didn’t end up leading the world in computing by luck. It happened because it made long-term, public investments in basic research, especially through NSF. That’s what created the technology that today’s companies are built on." / X
1/3 The US didn’t end up leading the world in computing by luck. It happened because it made long-term, public investments in basic research, especially through NSF. That’s what created the technology that today’s companies are built on.
x.com
May 31, 2025 at 5:16 PM
Reposted by Stephanie Weirich
There are 2 previous historical cases of countries destroying their science and universities, crippling them for decades: Lysenkoism in the USSR and Nazi Germany. The Trump administration will be the 3rd.
It's not just budgets but research, institutions, expertise, and training the next generation.
May 31, 2025 at 4:43 AM
Reposted by Stephanie Weirich
Defunding the NSF will have disastrous downstream effects on the tech industry. It’s time for people in industry to ACT. In this cross-post from the SIGARCH blog, Prof. Vijay Janapa Reddi outlines some steps you can take now. blog.sigplan.org/2025/05/19/t...
The Academic Pipeline Stall: Why Industry Must Stand for Academia
This post was cross-published from the SIGARCH blog. The Research Pipeline is Stalling The U.S. National Science Foundation (NSF) froze all outgoing funding, including new awards and scheduled…
blog.sigplan.org
May 19, 2025 at 1:49 PM
Reposted by Stephanie Weirich
(1/3) We are happy to announce the release of our POPL'25 coverage totaling 257 talks across POPL, CPP, VMCAI, PADL, and many more workshops and events!

www.youtube.com/@acmsigplan/...
ACM SIGPLAN
Special Interest Group on Programming Languages The ACM Special Interest Group on Programming Languages (SIGPLAN) explores programming language concepts and tools, focusing on design, implementation, ...
www.youtube.com
May 3, 2025 at 8:15 PM
Reposted by Stephanie Weirich
Thinking about devastating cuts to NSF: US gov-funded science has been the engine upon which most of the tech wealth was generated. But the oligarchs (currently hoarding much of that $) think it’s their own brilliance & not the accident of standing close to the scientific engine that made them rich.
May 4, 2025 at 5:47 PM
Reposted by Stephanie Weirich
Next week at ESOP 2025 (European Symposium on Programming) in Hamilton, ON (not in Europe) I'll be giving a talk on Stratified Type Theory! (Tue 6 May 10:30 am)
We replace stratified type universes with stratified judgements, and restrict dependent function domains to strictly smaller levels.
Stratified Type Theory
A hierarchy of type universes is a rudimentary ingredient in the type theories of many proof assistants to prevent the logical inconsistency resulting from combining dependent functions and the type-i...
arxiv.org
April 29, 2025 at 3:23 PM
Reposted by Stephanie Weirich
Lambda-join, a streaming functional language [1], implemented using minikanren's search strategy(!), in 3 variations: gist.github.com/rntz/9f0785244

[1] "Functional Meaning for Parallel Streaming"
Nick Rioux & Steve Zdancewic
PLDI 2025
arxiv.org/abs/2504.02975
Functional Meaning for Parallel Streaming
Nondeterminism introduced by race conditions and message reorderings makes parallel and distributed programming hard. Nevertheless, promising approaches such as LVars and CRDTs address this problem by...
arxiv.org
April 21, 2025 at 2:13 AM
Reposted by Stephanie Weirich
ICFP/SPLASH 2025 are seeking sponsors! This is a great opportunity to reach a broad audience, especially with the unique co-location of these two conferences this year.

conf.researchr.org/attending/ic...
Call for Sponsorship - ICFP/SPLASH 2025
Welcome to the website of the joint ICFP/SPLASH 2025 conference! For the first time, the two leading SIGPLAN venues—ICFP and SPLASH—will be co-located in Singapore in 2025: ICFP 2025: The ACM SI...
conf.researchr.org
February 11, 2025 at 9:43 PM
Reposted by Stephanie Weirich
I was reading this article written by CRA, wondering "now who *is* CRA?" Wondering if CRA was somehow just ACM, but it turns out CRA is in fact not just ACM and indeed has a very trustworthy executive board of some of the best folks in CS

cra.org/nsf-budget-c...
NSF Budget Cuts Would Put the Future of U.S. Innovation and Security at Risk
A statement from the Computing Research Association (CRA) Recent executive actions have raised the potential of significant budget cuts and mass layoffs at the National Science Foundation (NSF), a …
cra.org
February 9, 2025 at 2:28 AM
Reposted by Stephanie Weirich
Our POPL 2025 paper, Consistency of a Dependent Calculus of Indistinguishability, is officially out!
doi.org/10.1145/3704...
This is work by Yiyun Liu @ohqo.bsky.social, me, and Stephanie Weirich, proving consistency, normalization, and decidability of type checking for DCOIω. 1/3
Consistency of a Dependent Calculus of Indistinguishability | Proceedings of the ACM on Programming Languages
The Dependent Calculus of Indistinguishability (DCOI) uses dependency tracking to identify irrelevant arguments and uses indistinguishability during type conversion to enable proof irrelevance, suppor...
doi.org
January 10, 2025 at 10:17 PM