The following Scala code (Scala 3.8.0-RC1-bin-20250731-fe6b7eb-NIGHTLY, OpenJDK 21) - used in the EPFL CS-214 course - is a simple program that indefinitely plays a sound represented by a sine wave at 440Hz.

It first creates the sine as a LazyList, so that it is only evaluated when asked for. It can then play it. sine is effectively infinite: until it's stopped, the program will forever play the tune!

@main def main =
  val sine: LazyList[Sample] = loop(sinePulse(440))
  play(sine)

However, this program will quickly run into an issue and throw a runtime error... Can you see why?

A proof that passes can take forever at Qed time because of convertibility tests. Our proposed solution to this issue is to replay a computation trace instead of relying on heuristics.

Fixpoint boom n :=
  match n with
  | 0 => 0
  | S k => (if Nat.eqb n 24 then 1 else 0) + boom k + boom k
  end.

Goal 1 + (boom 50 + 1) = (1 + boom 50) + 1.
1 + (boom 50 + 1) = 1 + boom 50 + 1
Proof.
1 + (boom 50 + 1) = 1 + boom 50 + 1
  Time cbn -[boom]. (* immediate, should be replayed by Qed *)
Finished transaction in 0. secs (0.u,0.s) (successful)
S (boom 50 + 1) = S (boom 50 + 1)
  Time reflexivity. (* immediate *)
Finished transaction in 0. secs (0.u,0.s) (successful)
Fail Timeout 10 Qed. (* takes forever *)
The command has indeed failed with message:
Timeout!
Abort.

In a previous blogpost, Erik wrote about how he implemented the linear time matching algorithm from [RegElk+PLDI24] in the popular regex engine RE2. In this one, we're looking at how to do the same thing for the official regex engine from the Rust language. Namely, we add support for unbounded captureless lookbehinds.

This paper lays out a case study of Software Construction, a new course in the undergraduate computer and communication sciences curriculum at EPFL. We hope to share some generalizable lessons we learned from running its first edition in Fall 2023. The course targets three core concepts—functional programming, real-world engineering, and correctness—and its design is informed by four principles—students should learn by doing, assignments should be self-motivating, knowledge should be built incrementally, and students should see progress over time. We illustrate how we realized these concepts and principles with practical examples of course materials and teaching methods that we hope will serve as useful inspiration to others teaching similar courses. Lastly, we present some encouraging preliminary data about course outcomes and share our speculations about experiments for its future evolution.

Writing high-performance software these days is a challenging task. Today's hardware ecosystem is highly heterogeneous, with a trend towards application-tailored solutions. Despite years of effort in automation, by and large the burden still falls on the developer to write a program in a manner that can take advantage of this hardware. Oftentimes, the solution is to use a library carefully written by a performance engineer for the specific combination of application and hardware. But why is that? What happens when there is no library?

tl;dr: String diagrams are an intuitive diagrammatic representation of some pretty useful math. This being Interactive Theorem Proving, of course, I want to formalize that math in a proof assistant (Coq), in such a way that formal proofs still work like paper proofs using all the nifty properties of the diagrammatic representation. And, of course, a naïve formalization runs into problems that make the system painful to use. So this project explores how we might overcome those problems and restore the convenience of string diagrams in a formal setting.

Some programs use their data cache extensively, while underusing their instruction cache. We embed constant data, typically stored in memory, into the immediate fields of instructions to balance to use of both caches. We illustrate the impacts of such optimizations on the performances of a target program, describing the key parameters.

Specifications (such as RFCs, programming language standards) are typically written in natural language. To formally verify an implementation of such a spec, we need two things: a mechanization of the spec (in a theorem prover like Coq, Lean, Dafny, …), and a proof of correctness relating the implementation to the mechanized spec.

The correctness of the proof is guaranteed by the theorem prover. But who checks the correctness of the mechanization? The original spec is in natural language, so the best we can do is an audit. To make these audits easier, some specs are written in a “literate” style, with comments from the spec interleaved throughout the mechanization. This helps a lot, but… who checks the comments? In this post, I present SpecMerger, a tool that checks that literate comments match the spec they came from.

Modern regexes are fiendishly complex: beyond traditional features like alternations and loops, they include complex constructs such as backreferences, possessive groups, recursion, conditionals, or bounded (and sometimes even unbounded!) lookarounds.

Surprisingly, the complexity characteristics of these modern regex features are not fully known. Take lookarounds, for example: until recently, if you wanted a regex flavor that supported lookarounds, you had to use a backtracking-based algorithm.

Alectryon (named after the Greek god of chicken) is a collection of tools for writing technical documents that mix Coq code and prose, in a style sometimes called literate programming.

Coq proofs are hard to understand in isolation: unlike pen-and-paper proofs, proof scripts only record the steps to take (induct on x, apply a theorem, …), not the states (goals) that these steps lead to. As a result, plain proof scripts are essentially incomprehensible without the assistance of an interactive interface like CoqIDE or Proof General.

The most common approach these days for sharing proofs with readers without forcing them to run Coq is to manually copy Coq's output into source code comments — a tedious, error-prone, and brittle process. Any text that accompanies the proof is also embedded in comments, making for a painful editing experience.

Alectryon does better: it automatically captures Coq's output and interleaves it with proof scripts to produce interactive webpages, and it lets you toggle between prose- and code-oriented perspectives on the same document so that you can use your favorite text editing mode for writing prose and your favorite Coq IDE for writing proofs.

Most PL conferences moved online this year, and many are asking authors to pre-record talks to avoid livestreaming difficulties. Here are the steps we followed to record and edit our Kôika talk at PLDI 2020 and our extraction talk at IJCAR 2020. This posts covers preparing and recording the talk, adding the slides, and captioning the final video.

Let's say you've written a programming language in Coq. You have nice inductives for your ASTs; one for untyped terms (UntypedAST) and one for typed terms (TypedAST). You wrote a simple typechecker, and maybe an interpreter, too!

typecheck
     : UntypedAST -> option TypedAST
interp
     : TypedAST -> Value

You write a few programs…

Example well_typed := UAdd (UNat 1) (UNat 1).
Example ill_typed := UAdd (UNat 1) (UBool true).

… typecheck them:

Definition tc_good := typecheck well_typed.
Compute tc_good. (* Accepted: So far so good. *)
= Some
    {|
      tau := Nat; ast := TAdd (TNat 1) (TNat 1)
    |}
: option TypedAST

Definition tc_bad := typecheck ill_typed.
Compute tc_bad. (* Rejected: all good as well. *)
= None
: option TypedAST

… and attempt to run them:

Compute interp tc_good.
The term "tc_good" has type "option TypedAST"
while it is expected to have type "TypedAST".

D'oh! interp takes a TypedAST, but typecheck returns an option. What do we do?

A fairly common occurrence when working with dependent types in Coq is to call Compute on a benign expression and get back a giant, partially-reduced term, like this:

Import EqNotations Vector.VectorNotations.
Compute (Vector.hd (rew (Nat.add_1_r 3) in ([1; 2; 3] ++ [4]))).
= match
    match
      Nat.add_1_r 3 in (_ = H)
      return (Vector.t nat H)
    with
    | eq_refl => [1; 2; 3; 4]
    end as c in (Vector.t _ H)
    return
      (match
         H as c0 return (Vector.t nat c0 -> Type)
       with
       | 0 =>
           fun _ : Vector.t nat 0 =>
           False -> forall x1 : Prop, x1 -> x1
       | S x => fun _ : Vector.t nat (S x) => nat
       end c)
  with
  | [] =>
      fun x : False =>
      match
        x return (forall x0 : Prop, x0 -> x0)
      with
      end
  | h :: _ => h
  end
: (fun (n : nat) (_ : Vector.t nat (S n)) => nat)
    3
    (rew [Vector.t nat] Nat.add_1_r 3 in
     ([1; 2; 3] ++ [4]))

This post shows how to work around this issue.