Mastodawn

Just submitted my latest Swedish Science Council grant proposal: "Navigating the Incomparable"!

We want to build correct-by-construction software for multi-objective optimization—helping safely navigate complex trade-offs like economic costs vs. global temperature rise (see the attached idealised Pareto front).

To do this, we're proposing three connected work packages (see diagram) moving from formal specification, to state-space reduction, and finally scalable execution. We aim to combine #FunctionalProgramming, #DependentTypes, and dimensional analysis to build algebraically accountable tools for climate policy and fusion energy.

If funded, this opens a new PhD position in 2027!

📖 Read the full abstract: https://patrikja.owlstown.net/posts/5441

#Haskell #Agda #TypeTheory #ClimateScience #FusionEnergy #ProgLang

Tom de Jong 3d ago

I'm pleased, especially for our PhD student @aref_mz, that our paper "Generalized Decidability via Brouwer Trees" (https://arxiv.org/abs/2602.10844) with @aref_mz, @Nicolai_Kraus and @fnf was accepted to LICS'26.

#Agda was very useful for developing this work. Huge thanks to its maintainers!

My commiserations to those who submitted good work but didn't get in. I hope we can all escape this system one day.

Generalized Decidability via Brouwer Trees

In the setting of constructive mathematics, we suggest and study a framework for decidability of properties, which allows for finer distinctions than just "decidable, semidecidable, or undecidable". We work in homotopy type theory and use Brouwer ordinals to specify the level of decidability of a property. In this framework, we express the property that a proposition is $α$-decidable, for a Brouwer ordinal $α$, and show that it generalizes decidability and semidecidability. Further generalizing known results, we show that $α$-decidable propositions are closed under binary conjunction, and discuss for which $α$ they are closed under binary disjunction. We prove that if each $P(i)$ is semidecidable, then the countable meet $\forall i\in \mathbb N. P(i)$ is $ω^2$-decidable, and similar results for countable joins and iterated quantifiers. We also discuss the relationship with countable choice. All our results are formalized in Cubical Agda.

arXiv.org

Linotype Pilgrim 3d ago

Sadly, #Agda has not been able to adopt a sensible moratorium on slop entering the codebase. Several other proof assistants (Lean, Rocq) are also now corrupted by untrustworthy and plagiarised inputs. So much for commitment to rigour.

RE: https://bsky.app/profile/did:plc:osg2vzhifd2tjfsvfwua7scy/post/3mgdfho3x5k24

Jesper Agdakx 🔸6d ago

Our department is hiring an assistant professor in computer science (including programming languages). If you would like to join our small but diverse PL group in beautiful little Delft, please don't hesitate to apply! Also feel free to reach out to me if you want to know anything about our department or academic life in the Netherlands.

Deadline for applications: 11th of May

academictransfer.com/en/jobs/360114/assistant-professor-in-computer-science/

#TUDelft #AssistantProfessor #Hiring #ComputerScience #SoftwareTechnology #ProgrammingLanguages #TypeTheory #SoftwareVerification #Agda #Rocq

Assistant Professor in Computer Science

Develop the next generation of CS and AI intelligence technology that powers science and society at TU Delft. Combine research with real technological impact while educating talented students. Job description Are you inspired by shaping the next generation of…

AcademicTransfer

José A. Alonso Apr 10

Readings shared April 9, 2026. https://jaalonso.github.io/vestigium/posts/2026/04/10-readings_shared_04-09-26 #AI #AI4Math #ATP #Agda #FunctionalProgramming #ITP #IsabelleHOL #LeanProver #Math #Prover9

Readings shared April 9, 2026

The readings shared in Bluesky on 9 April 2026 are: ABC implies that Ramanujan's tau function misses almost all primes. ~ David Kurniadi Angdinata et als. #LeanProver #ITP #Math Do we need frontier m

Vestigium

José A. Alonso Apr 9

A graded modal dependent type theory with erasure, formalized. ~ Andreas Abel, Nils Anders Danielsson, Oskar Eriksson. https://arxiv.org/abs/2603.29716v1 #Agda #ITP

A Graded Modal Dependent Type Theory with Erasure, Formalized

We present a graded modal type theory, a dependent type theory with grades that can be used to enforce various properties of the code. The theory has $Π$-types, weak and strong $Σ$-types, natural numbers, an empty type, and a universe, and we also extend the theory with weak and strong unit types and graded $Σ$-types. The theory is parameterized by a modality structure, a kind of partially ordered semiring, whose elements (grades) are used to track the usage of variables in terms and types. Different modalities are possible. We focus mainly on quantitative properties, in particular erasure: with the erasure modality one can mark function arguments as erasable. The theory is fully formalized in Agda. The formalization, which uses a syntactic Kripke logical relation at its core and is based on earlier work, establishes major meta-theoretic properties such as subject reduction, consistency, normalization, and decidability of definitional equality. We also prove a substitution theorem for grade assignment, and preservation of grades under reduction. Furthermore we study an extraction function that translates terms to an untyped $λ$-calculus and removes erasable content, in particular function arguments with the "erasable" grade. For a certain class of modalities we prove that extraction is sound, in the sense that programs of natural number type have the same value before and after extraction. Soundness of extraction holds also for open programs, as long as all variables in the context are erasable, the context is consistent, and erased matches are not allowed for weak $Σ$-types.

arXiv.org

José A. Alonso Apr 5

Readings shared April 4, 2026. https://jaalonso.github.io/vestigium/posts/2026/04/04-readings_shared_04-04-26 #AI #AI4Math #ATP #Agda #AlphaProof #Autoformalization #CategoryTheory #CoqProver #FunctionalProgramming #ITP #IsabelleHOL #LLMs #LambdaCalculus #LeanProver #Lisp #Logic #LogicProgramming #LLMs #Math #Physics #Programming #Prolog #Racket #RocqProver #Vampire

Readings shared April 4, 2026

The readings shared in Bluesky on 4 April 2026 are: Why Lean?. ~ Leonardo de Moura. #LeanProver #ITP A formalization of the Gelfond-Schneider theorem. ~ Michail Karatarakis, Freek Wiedijk. #LeanProve

Vestigium

José A. Alonso Apr 4

Reseña de «A new paradigm for mathematical proof?». https://jaalonso.github.io/vestigium/posts/2025/11/08-a-new-paradigm-for-mathematical-proof/ #Math #ITP #LeanProver #Agda

Reseña de «A new paradigm for mathematical proof?»

En la conferencia «A new paradigm for mathematical proof?», Emily Riehl explora los desafíos actuales en la verificación de demostraciones matemáticas. Ejemplos como la conjetura de Kepler y el progra

Vestigium

amen zwa, esq.Mar 28

I am aghast to discover that “coding camp” type publications on proof assistants, like #Agda and #Lean, do exist, complete with the all-too-common modern #IT anthem, “No need to know any mathematics”, emblazoned across the introduction, and subsequent pages littered with code samples, without proofs.

There are two primary uses of a proof assistant: to do mathematics and to write verified programmes. Both uses are built upon writing formal proofs. Without writing proofs, a proof assistant is almost an inconvenient, inefficient #programming language.

Boyd Stephen Smith Jr.Mar 27

RE: https://hachyderm.io/@BoydStephenSmithJr/116298200584577447

Anyone out there with some opinions on both @codeberg and @gitlab particularly for developing #Haskell, #Idris, #Lean, or #Agda ? If you can,, please address my concerns in the quoted toot.