#agda

@jalonso.eurosky.social

10 hours 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

22 hours 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 week 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

2 weeks 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

2 weeks 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

2 weeks 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

2 weeks 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

3 weeks 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

1 month 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

1 month 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

2 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

2 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

2 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

3 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

3 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

3 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

3 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

0 1 0 0

José A. Alonso

@jalonso.eurosky.social

4 months ago

Readings shared November 14, 2025 The readings shared in Bluesky on 14 November 2025 are: An introduction to formal real analysis (Lecture 18: Rearrangements). ~ Alex Kontorovich. #ITP #LeanProver #Math Choice trees: Representing and

Readings shared November 14, 2025. jaalonso.github.io/vestigium/po... #AI #Agda #AlphaProof #CoqProver #FunctionalProgramming #Haskell #ITP #LeanProver #Math #OCaml #Rocq

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

4 months ago

Binary search—think positive | Journal of Functional Programming | Cambridge Core Binary search—think positive - Volume 35

Binary search—think positive. ~ Alexander Dinges, Ralf Hinze. www.cambridge.org/core/journal... #ITP #Agda

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

4 months ago

Towards type-directed compiler calculation | Journal of Functional Programming | Cambridge Core Towards type-directed compiler calculation - Volume 35

Towards type-directed compiler calculation. ~ Wouter Swierstra. www.cambridge.org/core/journal... #ITP #Agda

1 0 0 0

José A. Alonso

@jalonso.eurosky.social

4 months ago

Readings shared November 8, 2025 The readings shared in Bluesky on 8 November 2025 are: A new paradigm for mathematical proof? ~ Emily Riehl. #AI #Math #ITP #Agda #LeanProver An introduction to formal real analysis (Lecture 17: Seri

Readings shared November 8, 2025. jaalonso.github.io/vestigium/po... #AI #Agda #FunctionalProgramming #Haskell #ITP #LeanProver #Math

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

4 months ago

Emily Riehl, A New Paradigm for Mathematical Proof? | Natural Philosophy Symposium 2025 YouTube video by Hopkins Natural Philosophy Forum

A new paradigm for mathematical proof? ~ Emily Riehl. youtu.be/fzxW2XJS6SE #AI #Math #ITP #Agda #LeanProver

8 5 1 1

José A. Alonso

@jalonso.eurosky.social

4 months ago

Polynomial Universes in Homotopy Type Theory Awodey, later with Newstead, showed how polynomial functors with extra structure (termed ``natural models'') hold within them the categorical semantics for dependent type theory. Their work presented ...

Polynomial universes in Homotopy Type Theory. ~ C.B. Aberlé, David I. Spivak. arxiv.org/abs/2409.19176 #ITP #Agda #HoTT

2 0 0 0

Tim Makarios

@tmakarios.theres.life.ap.brid.gy

4 months ago

Original post on theres.life

I've been thinking about something that's related to Tarski's undefinability theorem (and might possibly be a corollary if viewed from the right angle), but relates to computability rather than truth. It seems to have implications for systems like Agda and Rocq, which I don't have much […]

0 0 0 0

Jencel Panic

@abuseofnotation.mathstodon.xyz.ap.brid.gy

4 months ago

Original post on mathstodon.xyz

All tutorials on dependent types talk about vectors and fail to mention that #agda uses dependent types in the id function:

(A: Set) -> A -> A

it accepts an argument of type Set (called A) and then the rest of the arguments depend on the value of A (i.e. the type that is given as an argument) […]

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

4 months ago