Master thesis by Maria Khakimova: "Enhancing Proof Assistant Error Messages with Hints: A User Study"

"We implemented hint enhancements for the error messages displayed upon three common mistakes: forgetting whitespace, using confusable Unicode characters, and supplying too few arguments to a function. A between-participants user study was then conducted with 70 students [..]"

https://repository.tudelft.nl/record/uuid:52513287-7149-41f1-a8e8-8e38696cb283

#Agda #DependentTypes #ProofAssistants #ErrorMessages #Usability #UserStudy #master #thesis

Extremely helpful exposition of Fin here by @jesper https://github.com/jespercockx/agda-lecture-notes/blob/master/agda.pdf. At long last, it feels as if I'm on the cusp of 'getting' #Agda ...

Phil Wadler will talk online in 15 mins (if I got the timezone right) on "Lambda, the Ultimate Teaching Assistant (Agda version)":

https://fme-teaching.github.io/2021/08/24/tutorial-series-of-the-fme-teaching-committee/

#agda #FormalMethods

Readings shared May 31, 2025. https://jaalonso.github.io/vestigium/posts/2025/05/31-readings_shared_05-31-25 #Agda #Coq #FunctionalProgramming #Haskell #HoTT #ITP #LeanProver #Logic #Math #Minlog #Rocq

Verifying Z3 RUP proofs with the interactive theorem provers Coq/Rocq and Agda. ~ Harry Bryant et als. https://msp.cis.strath.ac.uk/types2025/abstracts/TYPES2025_paper67.pdf #ITP #Coq #Rocq #Agda

Readings shared May 30, 2025. https://jaalonso.github.io/vestigium/posts/2025/05/30-readings_shared_05-30-25 #AIforCode #Agda #GenerativeAI #ITP #LeanProver #Math #Rocq

Agent-based logics in dependent type theory. ~ Colm Baston. https://colmbaston.uk/files/thesis.pdf #ITP #Agda

Readings shared May 29, 2025. https://jaalonso.github.io/vestigium/posts/2025/05/29-readings_shared_05-29-25 #AI #Agda #Coq #Emacs #ITP #IsabelleHOL #LeanProver #Lisp #Logic #Math

Formalising inductive and coinductive containers. ~ Stefania Damato, Thorsten Altenkirch, Axel Ljungström. https://arxiv.org/abs/2409.02603 #ITP #Agda

Mechanized safety of Jolteon consensus in Agda. ~ Orestis Melkonian, Mauro Jaskelioff, and James Chapman. https://msp.cis.strath.ac.uk/types2025/abstracts/TYPES2025_paper79.pdf #ITP #Agda

Readings shared May 20, 2025. https://jaalonso.github.io/vestigium/posts/2025/05/20-readings_shared_05-20-25 #Agda #Emacs #FunctionalProgramming #Haskell #HoTT #ITP #LeanProver #Logic #Math #OrgMode #Python #Rust #SAT_solvers #TypeTheory

Ordinal exponentiation in homotopy type theory. ~ Tom de Jong, Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu. https://arxiv.org/abs/2501.14542 #ITP #Agda #HoTT

OH on irc: "In a nutshell: #Agda is a programming language… 🧊 purely functional, free of mutable state 🐑 similar to Haskell in syntax and vibe 🧱 statically typed, so that many errors are caught at compile-time 🌳 familiar types like integers,lists,… 🧭 type inference" lets-play-agda.quasicoherent.io

Let's play Agda: running abstr...

@cbarrett I guess every place #Agda people hang out is a place where noobs hang out because nobody knows anything :D

2 votes for #agda
1.5 for #unison
.5 for #granule
1 for @pigworker ‘s new language that I can’t wait to read more about when it’s ready.

Thanks for the extra insight, my friends.

Believe it or not, I learned quite a bit about type theory just from this short poll (reading about Granule in particular).

Readings shared April 17, 2025. https://jaalonso.github.io/vestigium/posts/2025/04/17-readings_shared_04-17-25 #Agda #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LeanProver #Math

A readable and computable formalization of the Streamlet consensus protocol. ~ Mauro Jaskelioff, Orestis Melkonian, James Chapman. https://omelkonian.github.io/data/publications/formal-streamlet.pdf #ITP #Agda