Créer un compteSe connecter

Recherches récentes

Aucune recherche récente

Options de recherche

Disponible uniquement lorsque vous êtes connecté.
mastouille.fr est l'un des nombreux serveurs Mastodon indépendants que vous pouvez utiliser pour participer au fédiverse.
Mastouille est une instance Mastodon durable, ouverte, et hébergée en France.

Administré par :

Statistiques du serveur :

589
comptes actifs

mastouille.fr: À proposAnnuaire des profilsPolitique de confidentialité

Mastodon: À proposTélécharger l’applicationRaccourcis clavierVoir le code sourcev4.3.4

#agda

0 message0 participant0 message aujourd’hui
Public
Programming Languages Delft

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 [..]"

repository.tudelft.nl/record/u

#Agda#DependentTypes#ProofAssistants
Public
José A. Alonso

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

arXiv.orgOrdinal Exponentiation in Homotopy Type TheoryWhile ordinals have traditionally been studied mostly in classical frameworks, constructive ordinal theory has seen significant progress in recent years. However, a general constructive treatment of ordinal exponentiation has thus far been missing. We present two seemingly different definitions of constructive ordinal exponentiation in the setting of homotopy type theory. The first is abstract, uses suprema of ordinals, and is solely motivated by the expected equations. The second is more concrete, based on decreasing lists, and can be seen as a constructive version of a classical construction by Sierpiński based on functions with finite support. We show that our two approaches are equivalent (whenever it makes sense to ask the question), and use this equivalence to prove algebraic laws and decidability properties of the exponential. All our results are formalized in the proof assistant Agda.
Public *
Jesper Agdakx 🔸

As part of our (@sarantja@mastodon.social and yt) research on the usability of interactive theorem provers, we are conducting a study on the usage and state of tools and languages for type-driven development. We are interested in tools that encourage and facilitate type-driven development, especially in cases when they can help us reason about complex problems.

We are hoping to use your responses to identify the characteristic language features and tool interactions that enable type-driven development, with the eventual goals of enhancing them and bringing their benefits to a wider range of programmers.

Please fill in our anonymous, 10-minute survey here: https://tudelft.fra1.qualtrics.com/jfe/form/SV_bIsMxYTKUJkhVuS

You are welcome to participate if you have experience with any type-driven development tool, including dependently-typed languages (e.g., Coq, Lean, Agda), refinement types (e.g., Liquid Haskell), or even other static type systems (e.g., in Rust or Haskell).

P.S. In case you remember signing up for an interview with us in a previous survey and are now wondering whether that study will still go on, the answer is: yes! We’ve had to revise our schedule, but we are still excited to talk to you and will start inviting people for an interview soon.

tudelft.fra1.qualtrics.comType-Driven Development in PracticeUnderstanding the usage and state of tools and languages for Type-Driven Development
#Agda#Coq#Rocq
A répondu dans un fil de discussion
Public *
Tom de Jong

It turns out there is an even simpler example of a set that "fails" (in a much stronger sense) to have at most one tight apartness, following an idea of @aws.

Suppose ℕ has at most one tight apartness.
We show that double negation elimination (¬¬P ⇒ P for all P) holds.

Since ℕ is discrete (i.e. it has decidable equality), the relation ≠ is a tight apartness.

Let P be an arbitrary proposition.
The relation n ♯ m := P ∧ (n ≠ m) on ℕ is an apartness.
Furthermore, it is tight if we assume ¬¬P.
But it clearly coincides with ≠ if and only if P holds.

Thus, if the natural numbers have at most one tight apartness then double negation elimination, or equivalently excluded middle, holds.
Moreover, this generalizes to any discrete type with two distinct points.

The above is formalized in TypeTopology using #Agda, see martinescardo.github.io/TypeTo

martinescardo.github.ioApartness.Properties
A répondu dans un fil de discussion
Public
Tom de Jong

The above is all formalized in the #Agda TypeTopology development, see
martinescardo.github.io/TypeTo

A (topological) model of intuitionistic set theory validating WLPO but not LPO is given in the below paper (see its fifth page and Theorem 5.1 in particular).

Matt Hendtlass and Robert Lubarsky. 'Separating Fragments of WLEM, LPO, and MP'
The Journal of Symbolic Logic. Vol. 81, No. 4, 2016, pp. 1315-1343.
DOI: 10.1017/jsl.2016.38
URL: math.fau.edu/people/faculty/lu

martinescardo.github.ioApartness.Properties
Public
Tom de Jong

I'm pleased to advertise our latest paper titled "Ordinal Exponentiation in Homotopy Type Theory".
arxiv.org/abs/2501.14542

This is joint work with @fnf @Nicolai_Kraus and Chuangjie Xu.

All our results are formalized in Agda, building on @MartinEscardo's TypeTopology development, see the HTML version at ordinal-exponentiation-HoTT.gi
In particular, the Paper file links every numbered environment in the paper to its implementation in Agda.

arXiv.orgOrdinal Exponentiation in Homotopy Type TheoryWhile ordinals have traditionally been studied mostly in classical frameworks, constructive ordinal theory has seen significant progress in recent years. However, a general constructive treatment of ordinal exponentiation has thus far been missing. We present two seemingly different definitions of constructive ordinal exponentiation in the setting of homotopy type theory. The first is abstract, uses suprema of ordinals, and is solely motivated by the expected equations. The second is more concrete, based on decreasing lists, and can be seen as a constructive version of a classical construction by Sierpiński based on functions with finite support. We show that our two approaches are equivalent (whenever it makes sense to ask the question), and use this equivalence to prove algebraic laws and decidability properties of the exponential. All our results are formalized in the proof assistant Agda.
#logic#TypeTheory#HoTT
Public *
Jack

Hey all! I'm due for an (re-)introduction: I'm Jack, an engineer in the NYC area from a firmware & cybersecurity background, currently working in something like hardware-software co-design.

Technical work is often with #rust #kicad #python #verilog #c, and in all-too-rare moments stuff like #haskell #forth #agda and #prolog

I've never been much for social media, usually preferring to keep interests local: a better-detailed #introduction to follow as I figure this out 🙂

Public
Jesper Agdakx 🔸

The pre-print for the #ICPC paper “Pinpointing the Learning Obstacles of an Interactive Theorem Prover” by @sarantja @azaidman and yt is now available at https://sarajuhosova.com/assets/files/2025-icpc.pdf

I very much hope this will inspire more research on the usability and accessibility of the languages we build going forward!

Abstract:

Interactive theorem provers (ITPs) are programming languages which allow users to reason about and verify their programs. Although they promise strong correctness guarantees and expressive type annotations which can act as code summaries, they tend to have a steep learning curve and poor usability. Unfortunately, there is only a vague understanding of the underlying causes for these problems within the research community. To pinpoint the exact usability bottlenecks of ITPs, we conducted an online survey among 41 computer science bachelor students, asking them to reflect on the experience of learning to use the Agda ITP and to list the obstacles they faced during the process. Qualitative analysis of the responses revealed confusion among the participants about the role of ITPs within software development processes as well as design choices and tool deficiencies which do not provide an adequate level of support to ITP users. To make ITPs more accessible to new users, we recommend that ITP designers look beyond the language itself and also consider its wider contexts of tooling, developer environments, and larger software development processes.

#Agda#TheoremProving#DependentTypes
Public
José A. Alonso

Explicit weakening. ~ Philip Wadler. arxiv.org/abs/2412.03124 #ITP #Agda

arXiv.orgExplicit WeakeningI present a novel formulation of substitution, where facts about substitution that previously required tens or hundreds of lines to justify in a proof assistant now follow immediately - they can be justified by writing the four letters "refl". The paper is an executable literate Agda script, and source of the paper is available as an artifact in the file Weaken.lagda.md. Not all consequences of the pandemic have been awful. For the last three years, I've had the great pleasure of meeting with Peter Thiemann and Jeremy Siek for a couple of hours every week, via Zoom, exploring topics including core calculi, gradual typing, and formalisation in Agda. The work reported here arose from those discussions, and is dedicated to Peter on the occasion of his 60th birthday.
Public
Patrik Jansson

Here is Andreas Abel presenting a retrospective on 20 years of Agda (Implementors) Meetings. I have fond memories of the first few meetings back in the days when Ulf Norell and Nils Anders Danielsson were working on their PhD theses [and I was their thesis advisor]. I'm very grateful to all the developers and maintainers who have (and are still) spending time on making and improving Agda.

Fun fact: Ulf's PhD thesis [1] has now been cited [2] more than 1000 times (around 60 citations per year for 17 years).

[1] ncatlab.org/nlab/files/Norell-
[2] scholar.google.com/citations?v

@ulfnorell
#Agda
@jesper

Andreas Abel in front of the first slide of the "Twenty years of Agda Implementors Meetings" presentation at Chalmers.
Andreas Abel in front of a slide of the "Twenty years of Agda Implementors Meetings" presentation at Chalmers. The slide lists the meetings from the first 10 year period: from 2004 to 2014.
ExplorerFlux en direct
À propos