Lightnews — Scholar-powered news

José A. Alonso @jalonso.bsky.social · 7h

An empirical evaluation of property-based testing in Python. ~ Savitha Ravi, Michael Coblenz. dl.acm.org/doi/10.1145/... #Python #Programming

An Empirical Evaluation of Property-Based Testing in Python | Proceedings of the ACM on Programming Languages

Property-based testing (PBT) is a testing methodology with origins in the functional programming community. In recent years, PBT libraries have been developed for non-functional languages, including Python. However, to date, there is little evidence ...

dl.acm.org

1 1

José A. Alonso @jalonso.bsky.social · 7h

Proof repair across quotient type equivalences. ~ Cosmo Viola, Max Fan, Talia Ringer. dl.acm.org/doi/10.1145/... #ITP #Rocq

Proof Repair across Quotient Type Equivalences | Proceedings of the ACM on Programming Languages

Proofs in proof assistants like Rocq can be brittle, breaking easily in response to changes. To address this, recent work introduced an algorithm and tool in Rocq to automatically repair broken proofs in response to changes that correspond to type ...

dl.acm.org

José A. Alonso @jalonso.bsky.social · 7h

Incremental certified programming. ~ Tomás Díaz, Kenji Maillard, Nicolas Tabareau, Éric Tanter. dl.acm.org/doi/10.1145/... #ITP #Rocq

Incremental Certified Programming | Proceedings of the ACM on Programming Languages

Certified programming, as carried out in proof assistants and dependently-typed programming languages, ensures that a software meets its requirements by supporting the definition of both specifications and proofs. However, proofs easily break with ...

dl.acm.org

José A. Alonso @jalonso.bsky.social · 7h

Pyrosome: Verified compilation for modular metatheory. ~ Dustin Jamner, Gabriel Kammer, Ritam Nag, Adam Chlipala. dl.acm.org/doi/10.1145/... #ITP #CoqProver

Pyrosome: Verified Compilation for Modular Metatheory | Proceedings of the ACM on Programming Languages

We present Pyrosome, a generic framework for modular language metatheory that embodies a novel approach to extensible semantics and compilation, implemented in Coq. Common techniques for semantic reasoning are often tied to the specific structures of the ...

dl.acm.org

José A. Alonso @jalonso.bsky.social · 7h

Certified decision procedures for width-independent bitvector predicates. ~ Siddharth Bhat, Léo Stefanesco, Chris Hughes, Tobias Grosser. dl.acm.org/doi/abs/10.1... #ITP #LeanProver

Certified Decision Procedures for Width-Independent Bitvector Predicates | Proceedings of the ACM on Programming Languages

Bitvectors are foundational for automated reasoning. A few interactive theorem provers (ITP), such as Lean, have strong support for deciding fixed-width bitvector predicates by means of bitblasting. H...

dl.acm.org

José A. Alonso @jalonso.bsky.social · 8h

Deriving an Erlang interpreter from a mechanised formal semantics of core Erlang. ~ Gergő Lajos Turán, Arsenii Fomin, Péter Bereczky, Dániel Horpácsi, Simon Thompson. dl.acm.org/doi/abs/10.1... #ITP #Agda #FunctionalProgramming #Erlang

Deriving an Erlang Interpreter from a Mechanised Formal Semantics of Core Erlang | Proceedings of the 24th ACM SIGPLAN International Workshop on Erlang

dl.acm.org

1 3

José A. Alonso @jalonso.bsky.social · 8h

Don’t call us, we’ll call you (Towards mixed-initiative interactive proof assistants for programming language theory). ~ Jan Liam Verter, Tomas Petricek. tomasp.net/academic/pap... #ITP #Teaching

1

José A. Alonso @jalonso.bsky.social · 8h

Synthesizing implication lemmas for interactive theorem proving. ~ Ana Brendel, Aishwarya Sivaraman, Todd Millstein. dl.acm.org/doi/abs/10.1... #ITP #Rocq

Synthesizing Implication Lemmas for Interactive Theorem Proving | Proceedings of the ACM on Programming Languages

Interactive theorem provers (ITP) enable programmers to formally verify properties of their software systems. One burden for users of ITPs is identifying the necessary helper lemmas to complete a proof, for example those that define key inductive ...

dl.acm.org

José A. Alonso @jalonso.bsky.social · 8h

PVS formalization of proofs of the infinitude of primes. ~ Bruno Berto de Oliveira Ribeiro. bdm.unb.br/bitstream/10... #ITP #PVS #Math

José A. Alonso @jalonso.bsky.social · 8h

Checking a denotational semantics of Scheme in Agda. ~ Peter D. Mosses. dl.acm.org/doi/abs/10.1... #ITP #Agda

Checking a Denotational Semantics of Scheme in Agda | Proceedings of the 26th ACM SIGPLAN International Workshop on Scheme and Functional Programming

You will be notified whenever a record that you have chosen has been cited.

dl.acm.org

José A. Alonso @jalonso.bsky.social · 8h

Interactive theorem provers for proof education. ~ Romina Mahinpei, Manoel Horta Ribeiro, Mae Milano. dl.acm.org/doi/abs/10.1... #ITP #CoqProver #Teaching

Interactive Theorem Provers for Proof Education | Proceedings of the 2025 ACM SIGPLAN International Symposium on SPLASH-E

dl.acm.org

1 2

José A. Alonso @jalonso.bsky.social · 8h

Formalizing the zigzag construction of path spaces of pushouts. ~ Vojtěch Štěpančík. arxiv.org/abs/2510.084... #ITP #Agda

Formalizing the zigzag construction of path spaces of pushouts

A recent pre-print of Wärn gives a novel pen-and-paper construction of a type family characterizing the path spaces of an arbitrary pushout, and a natural language argument for its correctness. We pre...

arxiv.org

José A. Alonso @jalonso.bsky.social · 8h

Mechanised proofs of atom exhaustion in Erlang. ~ Arsenii Fomin, Péter Bereczky, Dániel Horpácsi, Gergő Lajos Turán. dl.acm.org/doi/pdf/10.1... #ITP #Rocq

José A. Alonso @jalonso.bsky.social · 8h

Freer arrows and why you need them in Haskell. ~ Grant VanDomelen, Gan Shen, Lindsey Kuper, Yao Li. dl.acm.org/doi/10.1145/... #Haskell #FunctionalProgramming

Freer Arrows and Why You Need Them in Haskell | Proceedings of the 18th ACM SIGPLAN International Haskell Symposium

You will be notified whenever a record that you have chosen has been cited.

dl.acm.org

3

José A. Alonso @jalonso.bsky.social · 8h

Lightweight testing of persistent amortized time complexity in the credit monad. ~ Anton Lorenzen. dl.acm.org/doi/10.1145/... #Haskell #FunctionalProgramming

Lightweight Testing of Persistent Amortized Time Complexity in the Credit Monad | Proceedings of the 18th ACM SIGPLAN International Haskell Symposium

You will be notified whenever a record that you have chosen has been cited.

dl.acm.org

José A. Alonso @jalonso.bsky.social · 8h

Automatic C bindings generation for Haskell. ~ Travis Cardwell, Sam Derbyshire, Edsko de Vries, Dominik Schrempf. dl.acm.org/doi/10.1145/... #Haskell #FunctionalProgramming

Automatic C Bindings Generation for Haskell | Proceedings of the 18th ACM SIGPLAN International Haskell Symposium

You will be notified whenever a record that you have chosen has been cited.

dl.acm.org

1

José A. Alonso @jalonso.bsky.social · 8h

Total type classes. ~ Robert Weingart, Nicolas Wu. dl.acm.org/doi/10.1145/... #Haskell #FunctionalProgramming

Total Type Classes | Proceedings of the 18th ACM SIGPLAN International Haskell Symposium

You will be notified whenever a record that you have chosen has been cited.

dl.acm.org

1

José A. Alonso @jalonso.bsky.social · 8h

Rebound: Efficient, expressive, and well-scoped binding. ~ Noé De Santo, Stephanie Weirich. dl.acm.org/doi/10.1145/... #Haskell #FunctionalProgramming

Rebound: Efficient, Expressive, and Well-Scoped Binding | Proceedings of the 18th ACM SIGPLAN International Haskell Symposium

You will be notified whenever a record that you have chosen has been cited.

dl.acm.org

1

José A. Alonso @jalonso.bsky.social · 8h

Plinth: A plugin-powered language built on Haskell. ~ Ziyang Liu, Kenneth MacKenzie, Roman Kireev, Michael Peyton Jones, Philip Wadler, Manuel Chakravarty. dl.acm.org/doi/10.1145/... #Haskell #FunctionalProgramming

Plinth: A Plugin-Powered Language Built on Haskell (Experience Report) | Proceedings of the 18th ACM SIGPLAN International Haskell Symposium

You will be notified whenever a record that you have chosen has been cited.

dl.acm.org

1

José A. Alonso @jalonso.bsky.social · 8h

The calculated typer (Functional pearl). ~ Zac Garby, Patrick Bahr, Graham Hutton. dl.acm.org/doi/10.1145/... #Haskell #FunctionalProgramming

The Calculated Typer (Functional Pearl) | Proceedings of the 18th ACM SIGPLAN International Haskell Symposium

You will be notified whenever a record that you have chosen has been cited.

dl.acm.org

1

José A. Alonso @jalonso.bsky.social · 8h

A Clash course in solving Sudoku (Functional pearl). ~ Gergő Érdi. dl.acm.org/doi/10.1145/... #Haskell #FunctionalProgramming

A Clash Course in Solving Sudoku (Functional Pearl) | Proceedings of the 18th ACM SIGPLAN International Haskell Symposium

You will be notified whenever a record that you have chosen has been cited.

dl.acm.org

José A. Alonso @jalonso.bsky.social · 9h

A tale of two lambdas: A haskeller’s journey into OCaml. ~ Richard A. Eisenberg. dl.acm.org/doi/10.1145/... #Haskell #OCaml #FunctionalProgramming

A Tale of Two Lambdas: A Haskeller’s Journey into OCaml (Keynote) | Proceedings of the 18th ACM SIGPLAN International Haskell Symposium

You will be notified whenever a record that you have chosen has been cited.

dl.acm.org

1

José A. Alonso @jalonso.bsky.social · 9h

Staging automatic differentiation with fusion. ~ Samuel Klumpers, Tom Schrijvers. dl.acm.org/doi/abs/10.1... #Haskell #FunctionalProgramming

Staging Automatic Differentiation with Fusion | Proceedings of the 18th ACM SIGPLAN International Haskell Symposium

dl.acm.org

1

José A. Alonso @jalonso.bsky.social · 9h

The conatural numbers form an exponential commutative semiring. ~ Szumi Xie, Viktor Bense. dl.acm.org/doi/10.1145/... #ITP #Agda #FunctionalProgramming

The Conatural Numbers Form an Exponential Commutative Semiring | Proceedings of the 10th ACM SIGPLAN International Workshop on Type-Driven Development

dl.acm.org

1

José A. Alonso @jalonso.bsky.social · 9h

A formalization of opaque definitions for a dependent type theory. ~ Nils Anders Danielsson, Eve Geng. dl.acm.org/doi/10.1145/... #ITP #Agda #FunctionalProgramming

1