#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 -
🔥 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 -
🔥 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 -
🔥 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 -
🔥 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 -
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 -
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 -
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 -
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.
