news

May 1, 2026

University of Rochester Takes Lean Kernel Arena Top Spot

Lean Kernel Leaderboard

The Lean Kernel Arena (arena.lean-lang.org) is a public benchmarking and testing ground for different proof checkers (kernels) used in the Lean Theorem Prover. It runs a large suite of tests to check the correctness of each checker and reports their speed (⏱️) and memory usage (🧠), especially on large, real-world tests like mathlib (the comprehensive Lean mathematical library). Below is a screenshot of the leaderboard taken on April 29, 2026.

The public ranking includes the official kernels alongside community alternatives based on nanoda (implemented in Rust), lean4lean (written in Lean itself), and rpylean (using just-in-time compiled Python). My PhD student, Yifan Zhu, and I began discussing cache optimization for nanoda a week ago. By Monday morning of this week, Yifan’s version of nanoda had reached the top spot! The techniques he used will be the subject of an upcoming technical report. In this blog, I am merely reporting the numbers, with some context for readers who may not be familiar with Lean.

The leaderboard reports performance in CPU time. In multi-threaded kernels, the wall-clock time may be significantly shorter due to parallelization. Yifan’s version shows only a 4% reduction in CPU time, but in wall-clock time, it is substantially faster. On the benchmark machine running four threads, the wall-clock times are 4.9 minutes for Yifan’s kernel, 6.3 minutes for the second fastest, and 22 minutes for the official version. Yifan’s Lean kernel is 22% faster than the second‑fastest kernel on the list.

Lean Applications

  • Formalizing mathematics. Lean has been used to formalize mathematical proofs, from undergraduate topics (calculus, linear algebra) to ongoing research. An April 2026 analysis counted over 308,000 declarations, 8.4 million logical connections, and almost 1.4 million lines of Lean code.
  • AI: Groups like Google DeepMind (with its AlphaProof system) use Mathlib as a benchmark and a knowledge base. AI models are trained on Mathlib’s data to learn how to reason and prove theorems automatically.

The most computationally demanding use cases are in the field of artificial intelligence, where AI models require generating and checking millions of potential proof steps. A faster kernel directly reduces the time and energy required to train and run these AI models. Beyond training AI, even standard automated proof tactics, e.g., simp (simplify) repeatedly applying rewriting rules to a goal, rely on kernel speed. With the rise of AI coding agents, the ability to quickly verify AI-generated code is crucial. An experimental AI agent was able to generate a 7,400-line verified embedded DSL over a single weekend, requiring the kernel to check thousands of lines of code for correctness on the fly (slides).

In industrial applications, speed is not just about cost-efficiency but about integrating verification directly into the development workflow. For example, AWS uses Lean to verify its Cedar policy system, ensuring no version ships unless all proofs pass. Microsoft uses Lean to verify its SymCrypt cryptographic library.

C++ vs Rust

I downloaded and counted the number of source lines in two kernels. The first is from https://github.com/leanprover/lean4.git in its src/kernel, counted using cloc:

This second is from https://github.com/ammkrn/nanoda_lib.git:

When measured in CPU time, the official C++ kernels take 30 to 40 minutes and use over 9 GB of memory. The Rust-based kernels, in contrast, take as little as 16.1 minutes in Yifan’s version and use half as much memory. In parallel (4-thread) executions, the wall-clock time is 22 minutes for the official version, compared to 4.9 and 6.3 minutes for the top two Rust-implemented kernels. The parallel speedup is less than 2× for the C++ kernels and 3.3× for Yifan’s kernel. Overall, the Rust kernels require less CPU time and show greater parallel efficiency than their C++ counterparts.

April 12, 2026

Programming Language Skills Are AI Skills

Because of AI, everyone needs to know programming languages

Jesen Huang in 2025

Jensen Huang famously said that with modern AI, the programming language becomes human language. Indeed, what used to take days to craft a program, AI tools can now write in seconds. Reports from the industry indicate that many senior engineers have not written a single line of code in months. However, AI coding is directed and managed by humans, and AI-generated code must be approved by humans. Code is cheap, but good code is not. In fact, more AI-generated code often means more human work. A compelling real-world example is the recent Anthropic source code leak, which highlights the risks associated with AI-assisted coding.

Fred Brooks in 1986

In his seminal article that laid the foundation for the field of software engineering, Frederick Brooks identified four essential difficulties of software development. He evaluated the solutions available at the time and concluded that while they addressed accidental difficulties, no solution could resolve the essential ones. He titled his article No Silver Bullet. The introduction begins:

Of all the monsters who fill the nightmares of our folklore, none terrify more than werewolves, because they transform unexpectedly from the familiar into horrors. For these, one seeks bullets of silver that can magically lay them to rest.

I imagine that Anthropic was probably horrified when their AI-generated system leaked over half a million lines of internal source code—a transformation from familiar tool to unexpected nightmare. Brook’s article is the required reading for the first week of the class I have been teaching. The first homework asks students to imagine talking to Jensen Huang and answering his question: “So, what are the essential difficulties of software?”

Programs Require Human Approval

Michael Scott, my colleague and the author of the popular textbook Programming Language Pragmatics, often quotes Donald Knuth: “Programming is the art of telling another human being what one wants the computer to do.” Part of this insight is that a program is a specification for a machine. In this regard, the key attribute is that a program must be precise. We should not—and must not—allow unspecified behavior by a machine. Think about programs that run laser eye surgeries, operate radiation machines, land jetliners, and control the ignition sequence to send Artemis II to the moon. We must write programs that are complete and precise.

AI has an unprecedented ability to automate programming, and its capabilities continue to improve. However, humans must be there to inspect and approve the generated code. The KPMG survey in Q3 2025 found that 63% of 130 executives said they are “putting humans in the loop due to a lack of trust, up from 45% last quarter.” In discussing the survey, one commenter explained that if people do not fully understand what a generated system does and why, they cannot defend it—not to a regulator, not to a client, and not to their leadership.

Precision is the foundation of reasoning. In mathematics, complete precision allows us to derive a result across a hundred steps while still knowing exactly what we are doing—and it enables someone to check every step along the way, a task that machines can now perform. Precision is the foundation of modern science and engineering. We can build complex systems today because we make every component fully precise.

The Conclusion: Everyone Needs to Know Programming Languages

With AI, modern programming may consist of three steps: (1) prompt AI to write code, (2) ensure the code is correct, and (3) explain to another human being what the code does and why it is correct. If Jensen Huang is correct that everyone will program using natural language, then it actually requires that everyone must know programming languages—because step (1) is fraught with risks without steps (2) and (3). Everyone needs to know programming languages enough to understand the code that they write using AI.

October 25, 2025

In Memoriam: Professor Tang, Shiwei (唐世渭) of PKU

Professor Tang was my undergraduate thesis advisor three decades ago. He passed away on Tuesday. Below is the English translation of the main passages of the article on Thursday in China’s Guangming Daily, full text in Chinese at https://mp.weixin.qq.com/s/JzjPkV0MMUjhlfibbRLNyw

Professor Tang Shiwei was born in December 1939 in Ningbo, Zhejiang Province. He graduated from the Computational Mathematics program of the Department of Mathematics and Mechanics at Peking University in 1964 and remained at the university to teach after graduation. He was promoted to professor in August 1990 and retired in December 2004.

Professor Tang Shiwei was a founder of the database as an academic discipline in China. He long dedicated himself to teaching and research in databases and information systems. He served as Director of the Database Research Laboratory in the Department of Computer Science and Technology at Peking University, Director of the Peking University Computing Center, Director of the Information Science Center, Director of the National Key Laboratory of Visual and Auditory Information Processing, Vice Chair of the Database Professional Committee of the China Computer Federation, and Professional Advisor to the Beijing Municipal People’s Government, making significant contributions to the development of computer science research and education in China.

At Peking University, he spearheaded the development of China’s independently copyrighted database management system, COBASE and the domestic system software platform COSA, for which COBASE was a key component and received a national award in 1996.

Original text in Chinese by Jin Haotian (晋浩天), correspondent, Guangming Daily

I took the database class around 1993, taught by his colleague Professor Yang, Dongqing (杨东清) and then joined their research group for my undergraduate thesis. I remember Professor Tang mentioning to me that they were the first in China to learn the development of databases in the US including reading the source code of early database systems. As a student assistant, I was sent to visit the Bank of China and talk to to account operators. It was pretty much deaf-mute conversation — I knew the textbook but nothing about applications let alone banking, but at the time I thought I was there to tell them what to do. Later a senior graduate student went to redo the visit. I was given part of the consulting fee even though my contribution might have been negative. Professor Tang was most generous and encouraging to me. I am fortunate and proud to be a part of his legacy.

Professor Tang also directed the undergrad thesis of Yuanyuan Zhou, now a professor at UCSD.

May 26, 2025

2025 CS Commencement Welcome

3:00 PM, May 17, 2025 | BAAC Auditorium

Dear Colleagues, parents, guests, and most important, our graduates:

Welcome to the 2025 CS graduation ceremony. I’m the department chair Professor Chen Ding.

Our 150 bachelor graduates and 30 MS graduates, here and elsewhere, you make today special: not just the day of graduation, but also the day we graduate the largest class in the department’s 50-year history.

At a commencement 20 years ago, David Foster Wallace told a parable: Two young fish swimming along, and they happen to meet an older fish swimming the other way, who nods at them and says, ‘Morning. How’s the water?’ And the two young fish swim on for a bit. Then one looks at the other and asks, ‘What is water?’

Parables are open to interpretation. So what is water the pervasive medium shaping our life? It is tech and increasingly CS. Computing principles drive every aspect from hardware to software to application. Blockchain, quantum computing, and autonomous driving all emerged from CS research. According U.S. Labor Statistics, over 60% of STEM jobs require CS skills. CS is transformative in other fields too. In this class, 96 undergrads, or almost two-thirds, took another major or minor.

Before going for his PhD, a student of mine plans to traverse the Continental Divide from El Paso, Texas, to Banff, Canada. Let his journey be not a symbol but embodiment of the grueling work of learning you did in the past and the daunting uncertainty of future you may be facing now.

Marcus Arellius said: Impediment to action advances action. Think 2700 miles, on a bike, alone, and camping under open skies. What stands in the way, becomes the way. Every challenge and setback is not blocking your path. It is the path. Our muscles strengthen, and our brain forms strong neural path ways when we work through our difficulties, none when things are easy.

You have done the hard work. What is the future?

CS is the engine of innovation. So much we have today did not exist even last year. This SSD card, a stamp in size, not much thicker, stores 1TB data. A question for parents and guests: raise your hand if you have used ChatGPT? An open-source equivalent is DeepSeek. You can download its data. The full model is 1TB. Most things we ask on Google you can now ask on ChatGPT or DeepSeek. Hence, information equivalent to Google Search is literally at my fingertip.

The power is immense majestic and terrifying. We see increasing inequality and political polarization at home, conflicts and wars abroad. CS is not innocent. Do you realize that we are the last generation who lived before social media? This little card tokenizes either human knowledge with unlimited potential or an existential threat, the ultimate FOOBAR.

This brings me to my final point, a last lesson if you will. A principle I teach in collaborative software design is that we are all fallible. Software is designed by people for people. Moral and human questions are infinitely more complex than math and science. There is no logical or mathematical certainty. The truth depends on a balance between two sets of conflicting reasons. It is crucial that you listen to people with whom you disagree, so you can go through the same mental journey they took to their conclusion. Quoting JS Mill: “In the human mind, one-sidedness has always been the rule, and many-sidedness the exception. Therefore, open our minds to listen to our opponents, thank them to do for us that otherwise we ought to do for ourselves.

To recap, everyone is fallible. We approach truth best by working together.

Speaking on behalf of all faculty and staff, congratulations. We will watch you with joy and pride. And we will always be here when you return to visit.

January 13, 2025

URCS 2024 in Rear View

Chair’s letter in the annual Multicast newsletter:

It is my pleasure and honor to succeed Michael Scott as the chair. We are an elite research department in a private university that excels in undergraduate education and advanced research. Our faculty size, 21 tenure track and 6 instructional, is substantial in size to lead research and teaching across broad topics in AI/HCI, systems, and theory, yet small enough to operate by consensus. This combination of size and strength is unique, making it the best department for me for over two decades. My goal for the three-year term is to maintain its quality, spirit, and momentum.

This is the year the department turns 50 and simultaneously grows young again. The department has grown steadily under Michael’s stewardship in the past four years, and Sandhya Dwarkadas’s before that. For the first time in over two decades, junior faculty outnumber senior faculty. The staff size is at an all-time high, and most administrative staff are recent hires. 

As part of the Meliora weekend, we celebrated our 50th anniversary with morning talks, an afternoon meet-and-greet, and an evening reception at the Hawkins-Carlson room at the library. Registration was beyond capacity for all three events, and the evening cocktail party was standing-room-only with a full house. Thanks to all who came to the celebration, especially our four keynote speakers: Danny Sabbah reminisced about how he fell asleep in his breakfast bowl after the grueling first-year exams; Amanda Stent defined modern AI as solving problems unsolvable by algorithms and then took questions for 24 minutes; Chris Stewart was as inspiring in his work, digital agriculture, as he was to me when he was in my advanced compiler class; and Michael Scott more than anyone embodied the department’s distinguished identity and stature, with grace and humor.

In the last year we have graduated 123 students with BA and BS degrees, 26 MS degrees, and 3 PhDs. While the PhD count is low after last year’s 20, two recent graduates started tenure track professorships, Jie Zhou (MS ’17, PhD ’23) at George Washington University and Michael Chavrimootoo (BS ’20, PhD ’24) at Denison University. Both worked with me on research prior to their successful PhD work – Jie Zhou on secure computing systems, directed by John Criswell, and Michael Chavrimootoo on computational social choice, directed by Lane Hemaspaandra. Michael also runs half marathons.

In technology, this is the year of generative AI. URCS was founded as an AI department, with five AAAI fellows on faculty over the years, including Henry Kautz, who was AAAI President from 2009 to 2014, and Len Schubert, who retired this summer after 37 years on the faculty most prominently in the field of common sense reasoning. The research of over half the department’s faculty is related to AI, with six professors specializing in core areas of statistical AI such as computer vision, natural language processing, graph neural networks, and machine learning theory, and teaching in these subjects. Next year, we plan to hire at least one additional AI faculty member. 

We are teaching a large number of students about AI. By my count, in the third week into Fall 2024, the department is teaching ten advanced courses (200 level or higher, 13 of which are cross-listed) to a total of 491 students, including 129 in CSC 242 Introduction to AI taught by Thaddeus Pawlicki; 99 in CSC 245/445 Deep Learning by Chenliang Xu who created the course in 2017; and 23 in CSC 511 Large Language Models, new this year created by Hangfeng He. Additional courses are offered by Data Science and Brain and Cognitive Science and have CS course numbers. 

Every year, our undergrads compete in the International Collegiate Programming Competition (ICPC). This year’s lead team consisting of Zeyu Nie ’24 (computer science and applied math), computer science master’s student Xiaoou Zhao, and Yan Zou ’27 (computer science) placed third in the regional, behind MIT and Harvard, and 17th in the North American Championship, just behind Michigan and Cornell. Despite competing against primarily schools with vastly larger CS programs, our students won their spot in the World Finals. In national contests, CS junior Cole Goodman won the NCAA Division III championship and qualified for the US Olympics Team Trials. Cole is the first Rochester student to do so since 1988 and the only athlete who has taken my course and learned computer organization and RISC-V assembly programming.

The department continues to work to broaden CS participation. Among the activities, ten students, led by our newest faculty member Yanan Guo, attended the Grace Hopper Celebration in October in Philadelphia, the largest gathering of women technologists worldwide. One month earlier, Fatemeh Nargesian led a ten-student group to San Diego, the largest in the department’s history, to the Tapia Conference, which annually brings together students, researchers, and professionals in computing from all backgrounds and ethnicities.

Last but not least, this is the year of charity giving. Danny Sabbah established the first endowed professorship in Computer Science with a generous $2M donation. Rick Rashid started the CS50th fund with a contribution of $100K. Since September 1, 2023, forty-seven other donors, mostly our graduates and their family members, have contributed a total of $38K. Charity is good for the soul. Intelligence may be mechanized, but the soul is uniquely human. The generous financial support is a confirmation from our alumni and others who care about the department, its mission, and its direction.

All that we do draws inspiration and strength from our alumni and friends. We are grateful for all your support.

With pride and gratitude, 

Chen Ding
Professor and Chair

January 24, 2022

Principles of Memory Hierarchy Optimization (PMHO) 2022

PPoPP Workshop on Principles of Memory Hierarchy Optimization (PMHO)

Video recordings of this year’s talks:

KEYNOTE: Advances in Modeling and Optimization of Caches. Don Towsley.

Random Walks on Huge Graphs at Cache Efficiency. Ke Yang.

CARL: Compiler Assigned Reference Leasing. Chen Ding.

Caching With Delayed Hits. Nirav Atre.

Delayed Hits in Multi-Level Caches. Benjamin Carleton.

A Study on Modeling and Optimization of Memory Systems. Xian-He Sun.

LHD: Improving Cache Hit Rate by Maximizing Hit Density. Nathan Beckmann.

On the Impact of Network Delays on Time-to-live Caching. Karim Elsayed.

Beyond Time Complexity: Data Movement Complexity Analysis for Matrix Multiplication. Wesley Smith.

Saturday 4/2/2022 1pm to 5pm US EDT (GMT -4), 6pm to 10pm Germany, 10:30pm to 2:30am India, 1am to 5am China, 2am to 6am Korea

Zoom Link: https://acm-org.zoom.us/j/92042756839?pwd=TllNMlVaeXQybkpWczh3ZnMxVDdFZz09
  Meeting ID/Passcode: 920 4275 6839 / PPoPP@2022

KEYNOTE

Recent Advances in the Modeling and Optimization of Caches

Donald F. Towsley, Distinguished Professor, University of Massachusetts Amherst

The keynote lecture covers the following results.

  1. An optimization-based approach to caching
  2. A simple, very accurate model of LRU and variants
  3. A new approach to bounding performance of caching policies based on a very simple ordering of failure rates of request distribution along with an application to on-line caching.  

The material is based on the following publications: Deghgan et al. “A Utility Optimization Approach to Network Cache Design,” IEEE/ACM Transactions on Networking, 27(3), 1013-1027, June 2019; “Sharing Cache Resources among Content Providers: A Utility-Based Approach,” IEEE/ACM Transactions on Networking, 27(2), 477-490, April 2019; Jiang et al. “On the Convergence of the TTL Approximation for an LRU Cache under Independent Stationary Request Processes”, ACM TOMPECS, 3(4), 20:1-20:31, September 2018; Panigrahy et al. “A new upper bound on cache hit probability for non-anticipative caching polices,” IFIP WG 7.3 Performance 2020; and Yan et al. “Learning from Optimal Caching for Content Delivery,” Proc. CoNEXT 2021, December 2021.

Workshop Program

PPoPP Workshop on Principles of Memory Hierarchy Optimization (PMHO)
Saturday 4/2/2022 1pm to 5pm US EDT (GMT -4), 6pm to 10pm Germany, 10:30pm to 2:30am India, 1am to 5am China, 2am to 6am Korea
Welcome and Introduction (1pm)
Keynote (1:10pm to 2:00pm)
Don Towsley: “Recent Advances in the Modeling and Optimization of Caches”.
Session 1 (2:00pm to 2:40pm)
Xian-He Sun: “A Study on Modeling and Optimization of Memory Systems”. JCST Jan. ’21. (2:00pm to 2:20pm)
Karim Elsayed: “On the Impact of Network Delays in Time-To-Live Caching”. Unpublished. (2:20pm to 2:40pm)
Break (2:40pm to 2:50pm)
Chen Ding: “CARL: Compiler Assigned Reference Leasing”. TACO March ’22. (2:50pm to 3:10pm).
Nirav Atre: “Caching with Delayed Hits”. SIGCOMM ’20. (3:10pm to 3:30pm)
Benjamin Carleton: “Evaluating the Impact of Delayed Hits in Multi-Level Caches”. SOSP ’21 SRC Undergraduate Winner. (3:30pm to 3:40pm).
Break (3:40pm to 3:50pm)
Nathan Beckmann: “LHD: Improving Cache Hit Rate by Maximizing Hit Density”. NSDI ’18. (3:50pm to 4:10pm)
Wesley Smith: “Beyond Time Complexity: Data Movement Complexity Analysis for Matrix Multiplication”. Under review. (4:10pm to 4:30pm)
Ke Yang (Video): “Random Walks on Huge Graphs at Cache Efficiency”. SOSP ’21. (4:30pm to 4:45pm)
Open discussion (4:45pm to 5:00pm)

For people who cannot attend, we plan to make the talk videos available as we have done in the 2021 workshop.

Organizers

Faculty:

  • Chen Ding, University of Rochester
  • Nathan Tallent, Pacific Northwest National Laboratory

Student:

  • Wesley Smith, University of Rochester

Call for Presentations

Data movement is now often the most significant constraint on speed, throughput, and power consumption for applications in a wide range of domains. Unfortunately, modern memory systems are almost always hierarchical, parallel, dynamically allocated and shared, making them hard to model and analyze. In addition, the complexity of these systems is rapidly increasing due to the advent of new technologies such as Intel Optane and high-bandwidth memory (HBM).

Conventional solutions to memory hierarchy optimization problems are often compartmentalized and heuristic-driven; in the modern era of complex memory systems these lack the rigor and robustness to be fully effective. Going forward, research on performance in the memory hierarchy must adapt, ideally creating theories of memory that aim at formal, rigorous performance and correctness models, as well as optimizations that are based on mathematics, ensure reproducible results, and have provable guarantees.

Format and Topics

PMHO is an annual specialized and topic-driven workshop to present ongoing, under review, or previously published work related to the following non-exhaustive topic list:

  • Mathematical and theoretical models of memory hierarchies including CPU/GPU/accelerator caches, software caching systems, key-value stores, network caches and storage system caches
  • Algorithmic and formal aspects of cache management including virtual memory
  • Programming models and compiler optimization of hierarchical complex memory systems

There will be no formal peer review process or publication, and presentations will be a mix of selections from submissions and invited presentations.

The 2022 workshop will take place online during the weekend of April 2 (Exact date TBD). It is hosted by the PPoPP 2022 conference.

Submission

Submit your presentation proposal to save-DyfTNd4RHy3y@3.basecamp.com. Submissions should consist of an one-page abstract of the topic you intend to present alongside any (optional) pertinent publications or preprints.

The submission deadline is Monday March 7, 2022 AOE.

February 16, 2019

Rahman Presenting at Compiler Construction Conference

Rahman was distilling the concept of spatial locality.  Prior to optimizing spatial locality in large scale code, Firefox, Chrome, LLVM, Rahman also developed the newest theory on optimal spatial locality in his paper in POPL 2016.

Rahman Lavaee, John Criswell, Chen Ding:
Codestitcher: Inter-Procedural Basic Block Layout Optimization.  in 28th International Conference on Compiler Construction, February 2019, Washington DC, USA.

December 29, 2017

2017 2nd URCSSA Alumni Summit

On Oct. 26, Dr. Chengliang Zhang, former graduate and now Staff Software Engineer at Google Seattle,  was invited by Chinese Student and Scholar Association (URCSSA) to speak at the second Alumni Summit titled Cloud | Big Data | AI.  The compiler group held a separate mini-symposium to present our research and had lunch with our esteemed graduate.

November 29, 2016

Robby Findler seminar and guest lecture

 

Macros matter: effectively building lots of programming languages
Robby Findler
Northwestern University & PLT
Monday, November 14, 2016

Building new programming languages from whole cloth is a difficult proposition at best. Macro system provide an alternative; they support the construction of new programming languages from existing pieces, while still providing the flexibility to radically change the syntax and semantics of the programming language.

In this talk, I will give a high-level overview of the myriad of programming languages that Racket supports, as well as an overview of the research area of macros, showing what can be accomplished with them and introducing some of the associated technical challenges (and their solutions).

Robby Findler is currently an Associate Professor at Northwestern University, and received his PhD from Rice University in 2002. His research area is programming languages and he focuses on programming environments, software contracts, and tools for modeling operational semantics. He maintains DrRacket, the program development environment for the programming language Racket and he co-authored the book _How to Design Programs_, a textbook for teaching introductory programming.

(URCS seminar announcement)

Slides

(CSC 253/453 Guest Lecture)  Redex: A Language for Lightweight Semantics Engineering

Professor Robby Findler, Northwestern University

Redex is a programming language designed to support semantics engineers as they experiment with programming language models.  To explore a model, an engineer writes down grammars, type systems, and operational semantics in a notation inspired by the programming languages literature. Redex breathes life into the model, building typing derivations, running example expressions, and using random generation to falsify claims about the model.

This talk gives an overview of Redex, motivating its design choices and giving a sense of how it feels to program in Redex. Then the talk dives into some of the techniques that Redex uses to generate random expressions.

A video by Prof. Findler on Redex

https://docs.racket-lang.org/redex/