#agda — Public Fediverse posts
Live and recent posts from across the Fediverse tagged #agda, aggregated by home.social.
-
So this was funny. My solver rederived theorems that had been marked as private because it predicted they'd be there. Twice. #agda
```
-- Made public 2026-05-02 (Step 1 of orbit-aware-completion-residue
-- arc): NSAHomReal2Complex re-derived `α*0` / `0*α` / `neg-0`
-- inline; Goal-T's `*-comm-ℂ` proof would re-derive them again.
-- Two re-derivations of identical content trigger RFS to expose
-- the originals. Behavior-preserving for existing callers.
``` -
Delooping generated groups in homotopy type theory. ~ Camil Champin, Samuel Mimram, Emile Oleon. https://arxiv.org/abs/2405.03264v1 #Agda #ITP #HoTT
-
CW: computer stuff, unproductive
Nice, now I can go back to being unproductive with #agda.
{ pkgs ? import <nixpkgs> { } }:
with pkgs;
mkShell {
buildInputs = [
(agda.withPackages (ps: [
ps.standard-library
]))
];
} -
Formalizing the real numbers in Homotopy Type Theory with Cubical Agda. ~ Jackson Brough. https://users.cs.utah.edu/~blg/resources/pdf/jackson-brough-cubicalreals-2026.pdf #Agda #ITP #Math
-
Finally finished a just-for-fun, completely-from-scratch constructive proof of the Fundamental Theorem of Arithmetic (just the existence part, not uniqueness (yet)) in #Agda. Took me about 10 hours and 750 lines of code. Fun times! Will probably turn it into a blog post at some point.
-
🔥 Ah, yes, the classic "let's throw neural networks and #types in a blender and see what mess comes out" approach. 🤖✨ The article rambles on about separating training and typechecking like it's some groundbreaking revelation, when really, it's just playing code Jenga with fancy names like #Idris, #Lean, and #Agda. 🧩🔍
https://www.brunogavranovic.com/posts/2026-04-20-types-and-neural-networks.html #neuralnetworks #codeJenga #HackerNews #ngated -
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
-
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
-
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
-
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
-
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
-
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.
-
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 -
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
-
A graded modal dependent type theory with erasure, formalized. ~ Andreas Abel, Nils Anders Danielsson, Oskar Eriksson. https://arxiv.org/abs/2603.29716v1 #Agda #ITP
-
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. 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. 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. 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. 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
-
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
-
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.
-
Want to learn more about the latest developments on using AI and (interactive) theorem proving in Mathematics? Wait no longer!
We have a great line-up of speakers at our online Workshop on AI and Theorem Provers in Mathematics. The workshop will be held online from 8th to 10th of April and attendance is free (registration required). For more details, visit the workshop website: https://aitpm.github.io/
#math #itp #theoremProving #isabelleHOL #lean #llm #ai #formal_mehods #agda #hol #mathematics
-
Readings shared March 14, 2026. https://jaalonso.github.io/vestigium/posts/2026/03/15-readings_shared_02-14-26 #AI #Agda #ITP #LeanProver #Math #Mizar
-
A formalization of abstract rewriting in Agda. ~ Sam Arkle, Andrew Polonsky. https://arxiv.org/abs/2603.10936v1 #Agda
-
The schedule for the 2026 PhD course "Functional Programming and Climate Impact Research" (FPClimate) is now live!
We kick off on March 23, reading and discussing papers on the application of FP, DSLs, and dependent types to climate modeling, decision problems, and policy advice.
Remote participation is available! External participants are very welcome to join the seminars and discussions (though we cannot issue formal university credits for externals).
Details & reading list: https://github.com/DSLsofMath/FPClimate
Blog post: https://patrikja.owlstown.net/posts/5275
#FunctionalProgramming #ClimateScience #Haskell #Agda #FormalMethods #AcademicMastodon
-
Readings shared February 24, 2026. https://jaalonso.github.io/vestigium/posts/2026/02/25-readings_shared_02-24-26 #AI4Math #ATP #Agda #CoqProver #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Math #Reasoning #Vampire
-
When Agda met Vampire. ~ Artjoms Šinkarovs, Michael Rawson. https://arxiv.org/abs/2602.18844v1 #Agda #ITP #Vampire #ATP
-
Formalized run-time analysis of active learning - coalgebraically in Agda. ~ Thorsten Wißmann. https://arxiv.org/abs/2602.16427 #Agda #ITP
-
Classifying 2-groups in Homotopy Type Theory. ~ Perry Hart, Owen Milner. https://phart3.github.io/2-groups-preprint.pdf #Agda #ITP
-
The Agda standard library has been published in the Journal of Open Source Software. Congratulations to Matthew Daggitt, @gallais , James McKinna, Andreas Abel, @Taneb , @mudri , Ulf Norell, @oisdk, Sergei Meshveliani, Sandro Stucki, @JacquesC2, Alex Rice, Jason Hu, Li-yao Xia, Shu-Hung You, @totbwf and @wen !
joss.theoj.org/papers/10.21105/joss.09241
#Agda #ITP #DependentTypes #JOSS #OSS -
Readings shared December 29, 2025. https://jaalonso.github.io/vestigium/posts/2025/12/30-readings_shared_12-29-25 #AI #Agda #CoqProver #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LeanProver #Logic #Math #OCaml #Rocq #SMT
-
Annals of Formalized Mathematics: un nouvel épi-journal dédié à la formalisation. https://www.insmi.cnrs.fr/fr/cnrsinfo/annals-formalized-mathematics-nouvel-epijournal-formalisation #ITP #Math #LeanProver #IsabelleHOL #Rocq #Agda
-
Readings shared November 7, 2025. https://jaalonso.github.io/vestigium/posts/2025/11/08-readings_shared_11-07-25 #AI #Agda #AlphaEvolve #FormalVerification #FunctionalProgramming #Haskell #HoTT #ITP #LLM #LeanProver #Math #Rocq
-
Polynomial universes in Homotopy Type Theory. ~ C.B. Aberlé, David I. Spivak. https://arxiv.org/abs/2409.19176 #ITP #Agda #HoTT
