#agda

@jalonso.eurosky.social

2 hours ago

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.

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

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

4 days ago

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

Readings shared April 4, 2026. jaalonso.github.io/vestigium/po... #AI #AI4Math #ATP #Agda #Autoformalization #CategoryTheory #CoqProver #FunctionalProgramming #ITP #IsabelleHOL #LLMs #LambdaCalculus #LeanProver #Lisp #Logic #LogicProgramming #LLMs #Math #Programming #Prolog #Racket #RocqProver

2 0 0 0

José A. Alonso

@jalonso.eurosky.social

5 days ago

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

Reseña de «A new paradigm for mathematical proof?». jaalonso.github.io/vestigium/po... #Math #ITP #LeanProver #Agda

1 0 0 0

Boyd Stephen Smith Jr.

@boydstephensmithjr.hachyderm.io.ap.brid.gy

1 week ago

RE: hachyderm.io/@BoydStephenSmithJr/1162...

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.

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

3 weeks ago

Readings shared March 14, 2026 The readings shared in Bluesky on 14 March 2026 are: From SMT solvers to Lean and the future of automated reasoning. ~ Leo de Moura, Nicola Gigante. #LeanProver #ITP A formalization of Borel determin

Readings shared March 14, 2026. jaalonso.github.io/vestigium/po... #AI #Agda #ITP #LeanProver #Math #Mizar

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

3 weeks ago

A Formalization of Abstract Rewriting in Agda We present a constructive formalization of Abstract Rewriting Systems (ARS) in the Agda proof assistant, focusing on standard results in term rewriting. We define a taxonomy of concepts related to ter...

A formalization of abstract rewriting in Agda. ~ Sam Arkle, Andrew Polonsky. arxiv.org/abs/2603.109... #Agda

2 1 0 0

Linotype Pilgrim

@symbo1ics.bsky.social

1 month ago

Core #Agda language maintainer punts LLM slop from the project:

"As a human being, you should also reject LLM salespeople, and the garbage they dump in our repository, for a variety of social reasons, including basic decency. …It is no coincidence that the logo of every LLM company is a butthole."

7 0 2 0

José A. Alonso

@jalonso.eurosky.social

1 month ago

Readings shared February 24, 2026 The readings shared in Bluesky on 24 February 2026 are: Formalizing Gröbner basis theory in Lean. ~ Junyu Guo, Hao Shen, Junqi Liu, Lihong Zhi. #LeanProver #ITP #Math Integral curves and flows on Ban

Readings shared February 24, 2026. jaalonso.github.io/vestigium/po... #AI4Math #ATP #Agda #CoqProver #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Math #Reasoning #Vampire

1 0 0 0

José A. Alonso

@jalonso.eurosky.social

1 month ago

When Agda met Vampire Dependently-typed proof assistants furnish expressive foundations for mechanised mathematics and verified software. However, automation for these systems has been either modest in scope or complex in ...

When Agda met Vampire. ~ Artjoms Šinkarovs, Michael Rawson. arxiv.org/abs/2602.188... #Agda #ITP #Vampire #ATP

2 1 0 0

José A. Alonso

@jalonso.eurosky.social

1 month ago

Formalized Run-Time Analysis of Active Learning -- Coalgebraically in Agda The objective of automata learning is to reconstruct the implementation of a hidden automaton, to which only a teacher has access. The learner can ask certain kinds of queries to the teacher to gain m...

Formalized run-time analysis of active learning - coalgebraically in Agda. ~ Thorsten Wißmann. arxiv.org/abs/2602.16427 #Agda #ITP

2 0 0 0

José A. Alonso

@jalonso.eurosky.social

1 month ago

Classifying 2-groups in Homotopy Type Theory. ~ Perry Hart, Owen Milner. phart3.github.io/2-groups-pre... #Agda #ITP

2 0 0 0

Linotype Pilgrim

@symbo1ics.bsky.social

1 month ago

Programming Language Foundations in Agda – Table of Contents

OH "you might find it fun to pick up #Agda. similar enough to Haskell to get started; different enough to be interesting plfa.github.io "

#plt

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

1 month ago

Readings shared February 14, 2026 The readings shared in Bluesky on 14 February 2026 are: Formalization of the Golay-Hopf machine: A unified algebraic framework for Hida, Iwasawa, and Yang-Baxter structures. ~ Yoshihiro Hasegawa. #IT

Readings shared February 14, 2026. jaalonso.github.io/vestigium/po... #AI4Math #Agda #Clojure #CoqProver #FunctionalProgramming #Haskell #ITP #LeanProver #Lisp #Logic #Math #Minlog #Prolog #RustLang

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

1 month ago

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". W...

Generalized decidability via Brouwer trees. ~ Tom de Jong, Nicolai Kraus, Aref Mohammadzadeh, Fredrik Nordvall Forsberg. arxiv.org/abs/2602.108... #Agda #ITP

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

2 months ago

Commutative algebras of series We consider a large family of product operations of formal power series in noncommuting indeterminates, the classes of automata they define, and the respective equivalence problems. A $P$-product of s...

Commutative algebras of series. ~ Lorenzo Clemente. arxiv.org/abs/2601.198... #ITP #Agda #Math

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

2 months ago

The Leibniz adjunction in homotopy type theory, with an application to simplicial type theory Simplicial type theory extends homotopy type theory and equips types with a notion of directed morphisms. A Segal type is defined to be a type in which these directed morphisms can be composed. We sho...

The Leibniz adjunction in homotopy type theory, with an application to simplicial type theory. ~ Tom de Jong, Nicolai Kraus, Axel Ljungström. arxiv.org/abs/2601.218... #ITP #Agda

0 0 0 0

Boyd Stephen Smith Jr.

@boydstephensmithjr.hachyderm.io.ap.brid.gy

2 months ago

Original post on hachyderm.io

Hey, any #idris or #agda people also see that "simple trick" for carrying around the index equalities necessary for a hetrogenous equality?

Like, the equality proof I'm building is something like [not real syntax] (x : RVect n Mine) = (y : RVect (n + 0) Mine).

Trying to pattern-match on the […]

0 0 1 0

José A. Alonso

@jalonso.eurosky.social

3 months ago

Readings shared December 29, 2025 The readings shared in Bluesky on 29 December 2025 are: Hint-based SMT proof reconstruction. ~ Joshua Clune, Haniel Barbosa, Jeremy Avigad. #ITP #LeanProver #SMT The biggest controversy in maths coul

Readings shared December 29, 2025. jaalonso.github.io/vestigium/po... #AI #Agda #CoqProver #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LeanProver #Logic #Math #OCaml #Rocq #SMT

1 0 0 0

José A. Alonso

@jalonso.eurosky.social

3 months ago

NAMOR: a new Agda library for modal extended sequents. ~ Riccardo Borsetto, Margherita Zorzi. ceur-ws.org/Vol-4142/pap... #ITP #Agda

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

3 months ago

Algebraizing higher-order effects. ~ Martin Andrieux, Alan Schmitt. hal.science/hal-05428166... #ITP #Agda

0 0 0 0

VP(WP)

@vpavlyshyn.bsky.social

4 months ago

The Geometry of Knowledge: How Cubic Types Reveal the Hidden Architecture of Metagraphs

#agda #cubictypes #metagraphs #ai

1 0 0 0

VP(WP)

@vpavlyshyn.bsky.social

4 months ago

Open World vs Closed World: Modeling OWL and SHACL Semantics in Agda

#ontology #schacl #agda #graphs #ai

2 0 0 0

José A. Alonso

@jalonso.eurosky.social

4 months ago

Readings shared November 23, 2025 The readings shared in Bluesky on 23 November 2025 are: DeepMind’s latest: An AI for handling mathematical proofs. ~ Jacek Krywko. #AI #Math #LLMs #ITP #LeanProver #AlphaProof Verified certification

Readings shared November 23, 2025. jaalonso.github.io/vestigium/po... #AI #Agda #AlphaProof #FunctionalProgramming #ITP #IsabelleHOL #LLMs #LeanProver #Math #OCaml #Rocq

1 0 0 0

José A. Alonso

@jalonso.eurosky.social

4 months ago

Annals of Formalized Mathematics: un nouvel épi-journal dédié à la formalisation. www.insmi.cnrs.fr/fr/cnrsinfo/... #ITP #Math #LeanProver #IsabelleHOL #Rocq #Agda