#liquidhaskell — Public Fediverse posts

Readings shared October 15, 2025. https://jaalonso.github.io/vestigium/posts/2025/10/16-readings_shared_10-15-25 #AI #CoqProver #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #LiquidHaskell #Math #OCaml #Rocq

Readings shared October 15, 2025. https://jaalonso.github.io/vestigium/posts/2025/10/16-readings_shared_10-15-25 #AI #CoqProver #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #LiquidHaskell #Math #OCaml #Rocq

Verifying the functional correctness of Braun trees with LiquidHaskell. ~ Felipe de León, Alberto Pardo, Marcos Viera. https://systemf.epfl.ch/etc/vstte2025/preprints/Verifying%20the%20Functional%20Correctness%20of%20Braun%20Trees%20with%20LiquidHaskell.pdf #Haskell #FunctionalProgramming #LiquidHaskell

Verifying the functional correctness of Braun trees with LiquidHaskell. ~ Felipe de León, Alberto Pardo, Marcos Viera. https://systemf.epfl.ch/etc/vstte2025/preprints/Verifying%20the%20Functional%20Correctness%20of%20Braun%20Trees%20with%20LiquidHaskell.pdf #Haskell #FunctionalProgramming #LiquidHaskell

Feeling great about my recent post @tweag's software engineering blog!

It tells the story of how (and why) I implemented qualified identifier support for refinement type aliases in #LiquidHaskell during my participation at #GSoC 2025.

Check it out!

https://www.tweag.io/blog/2025-09-11-qualified-aliases/

@haskell_foundation
#Haskell

Feeling great about my recent post @tweag's software engineering blog!

It tells the story of how (and why) I implemented qualified identifier support for refinement type aliases in #LiquidHaskell during my participation at #GSoC 2025.

Check it out!

https://www.tweag.io/blog/2025-09-11-qualified-aliases/

@haskell_foundation
#Haskell

Just wrapped up the first half of my GSoC project on improving name resolution in Liquid Haskell (LH)! It’s been lots of fun—long hours of code reading, analysis, testing, and debugging. Not that those were the most exciting parts, but pushing through and gaining a deeper understanding of the system definitely was.

LH hooks into the compiler pipeline to turn special comment annotations (refining types using logical predicates) into constraints for an external SMT solver to check. My project focuses on a very narrow feature, but along the way I’ve run into all sorts of cool programming concepts—like generic traversals of data structures and strongly connected components in directed graphs—while working through the parsing, name resolution, and definition unfolding implementations.

I’m deeply grateful to Facundo Domínguez for his generous and thoughtful mentoring, which has made this a rich learning experience and given me valuable engineering insights. I expect new challenges ahead, but I’ll do my best to sneak in some optimizations and give legacy code a proper cleanup.

https://summerofcode.withgoogle.com/programs/2025/projects/ALSN6wwr

#Haskell #GHC #LiquidHaskell #GSoC

Just wrapped up the first half of my GSoC project on improving name resolution in Liquid Haskell (LH)! It’s been lots of fun—long hours of code reading, analysis, testing, and debugging. Not that those were the most exciting parts, but pushing through and gaining a deeper understanding of the system definitely was.

LH hooks into the compiler pipeline to turn special comment annotations (refining types using logical predicates) into constraints for an external SMT solver to check. My project focuses on a very narrow feature, but along the way I’ve run into all sorts of cool programming concepts—like generic traversals of data structures and strongly connected components in directed graphs—while working through the parsing, name resolution, and definition unfolding implementations.

I’m deeply grateful to Facundo Domínguez for his generous and thoughtful mentoring, which has made this a rich learning experience and given me valuable engineering insights. I expect new challenges ahead, but I’ll do my best to sneak in some optimizations and give legacy code a proper cleanup.

https://summerofcode.withgoogle.com/programs/2025/projects/ALSN6wwr

#Haskell #GHC #LiquidHaskell #GSoC

As part of our (@[email protected] 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.

#Agda #Coq #Rocq #Lean #LiquidHaskell #Rust #Haskell #TypeDrivenDevelopment #TyDe #DependentTypes #LiquidTypes #RefinementTypes #ProofAssistants #Survey

As part of our (@[email protected] 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.

#Agda #Coq #Rocq #Lean #LiquidHaskell #Rust #Haskell #TypeDrivenDevelopment #TyDe #DependentTypes #LiquidTypes #RefinementTypes #ProofAssistants #Survey

... #LiquidHaskell (restriction types, SMT solver) and the Isabelle proof assistant.

For example, look at the kind of assurances we can make about data at the type-level. This means the SMT solver can assure that certain logical constraints on types are provably true.

My code to verify a file ranking algo I made:

https://github.com/someodd/bore/blob/master/src/Bore/SpacecookieClone/Search/Verified.hs

... #LiquidHaskell (restriction types, SMT solver) and the Isabelle proof assistant.

For example, look at the kind of assurances we can make about data at the type-level. This means the SMT solver can assure that certain logical constraints on types are provably true.

My code to verify a file ranking algo I made:

https://github.com/someodd/bore/blob/master/src/Bore/SpacecookieClone/Search/Verified.hs

Readings shared September 13, 2024. https://jaalonso.github.io/vestigium/posts/2024/09/13-readings_shared_09-13-24 #Haskell #FunctionalProgramming #LiquidHaskell #Emacs #OrgMode

Readings shared September 13, 2024. https://jaalonso.github.io/vestigium/posts/2024/09/13-readings_shared_09-13-24 #Haskell #FunctionalProgramming #LiquidHaskell #Emacs #OrgMode

Reflecting away from definitions in Liquid Haskell. ~ Jonathan Arnoult. https://www.tweag.io/blog/2024-09-12-lh-reflection #Haskell #FunctionalProgramming #LiquidHaskell

Reflecting away from definitions in Liquid Haskell. ~ Jonathan Arnoult. https://www.tweag.io/blog/2024-09-12-lh-reflection #Haskell #FunctionalProgramming #LiquidHaskell

Lecturas compartidas el 21 de julio de 2024. https://jaalonso.github.io/vestigium/posts/2024/07/22-lecturas_compartidas_el_21-jul-24 #ITP #IsabelleHOL #Coq #Logic #Math #FunctionalProgramming #Haskell #LiquidHaskell

Lecturas compartidas el 21 de julio de 2024. https://jaalonso.github.io/vestigium/posts/2024/07/22-lecturas_compartidas_el_21-jul-24 #ITP #IsabelleHOL #Coq #Logic #Math #FunctionalProgramming #Haskell #LiquidHaskell

Liquid amortization: Proving amortized complexity with LiquidHaskell (Functional pearl). ~ Jan van Brügge. https://arxiv.org/abs/2407.13671 #FunctionalProgramming #Haskell #LiquidHaskell

Liquid amortization: Proving amortized complexity with LiquidHaskell (Functional pearl). ~ Jan van Brügge. https://arxiv.org/abs/2407.13671 #FunctionalProgramming #Haskell #LiquidHaskell

Lecturas compartidas el 18 de julio de 2024. https://jaalonso.github.io/vestigium/posts/2024/07/19-lecturas_compartidas_el_18-jul-24 #ITP #Coq #IsabelleHOL #FunctionalProgramming #Haskell #LiquidHaskell #AI #ChatGPT #Math

Lecturas compartidas el 18 de julio de 2024. https://jaalonso.github.io/vestigium/posts/2024/07/19-lecturas_compartidas_el_18-jul-24 #ITP #Coq #IsabelleHOL #FunctionalProgramming #Haskell #LiquidHaskell #AI #ChatGPT #Math

Modular implementation and formalization of dynamic policies (Work in progress). ~ Antonio Zegarelli, Niki Vazou, Marco Guarnieri. https://fcs-workshop.github.io/fcs2024/papers/FCS_Zegarelli_Vazou_Guarnieri.pdf #FunctionalProgramming #LiquidHaskell

Modular implementation and formalization of dynamic policies (Work in progress). ~ Antonio Zegarelli, Niki Vazou, Marco Guarnieri. https://fcs-workshop.github.io/fcs2024/papers/FCS_Zegarelli_Vazou_Guarnieri.pdf #FunctionalProgramming #LiquidHaskell

Lecturas compartidas el 31 de mayo de 2024. https://jaalonso.github.io/vestigium/posts/2024/06/01-lecturas_compartidas_el_31-may-24 #ITP #Lean4 #IsabelleHOL #Math #FunctionalProgramming #LiquidHaskell

Lecturas compartidas el 31 de mayo de 2024. https://jaalonso.github.io/vestigium/posts/2024/06/01-lecturas_compartidas_el_31-may-24 #ITP #Lean4 #IsabelleHOL #Math #FunctionalProgramming #LiquidHaskell

Liquid Haskell through the compilers. ~ Facundo Domínguez. https://www.tweag.io/blog/2024-05-30-lh-upgrades/ #FunctionalProgramming #LiquidHaskell

Liquid Haskell through the compilers. ~ Facundo Domínguez. https://www.tweag.io/blog/2024-05-30-lh-upgrades/ #FunctionalProgramming #LiquidHaskell

I'm going to use #nixpkgs for now and ignore #liquidhaskell at the moment, sadly.

Spending more time on #nixpkgs than coding in #haskell again. Feel motivated to get #liquidhaskell working.

It's sad that #liquidhaskell is broken (liquidpoint marked as broken?) in #nixpkgs right now (right?).

Anyone know what's up with that?

I am yet again starting a project in #haskell and having fun getting lost in something fun, but basically causing me to be side-tracked.

I'm working on a simple pixel art editor, but I am excited by #LiquidHaskell to, I think, use refinement types and prove certain properties about my code.

I am yet again starting a project in #haskell and having fun getting lost in something fun, but basically causing me to be side-tracked.

I'm working on a simple pixel art editor, but I am excited by #LiquidHaskell to, I think, use refinement types and prove certain properties about my code.

Learning about #LiquidHaskell!

Have any of you used LiquidHaskell?

Towards a translation from Liquid Haskell to Coq. ~ Lykourgos Mastorou, Niki Vazou, Michael Greenberg. https://types2023.webs.upv.es/TYPES2023.pdf#page=125 #ITP #LiquidHaskell #Coq

Towards a translation from Liquid Haskell to Coq. ~ Lykourgos Mastorou, Niki Vazou, Michael Greenberg. https://types2023.webs.upv.es/TYPES2023.pdf#page=125 #ITP #LiquidHaskell #Coq

Assumptions for Liquid Haskell in the large. ~ Facundo Domínguez. https://www.tweag.io/blog/2023-06-22-lh-assumption-imports/ #Haskell #LiquidHaskell #FunctionalProgramming

Assumptions for Liquid Haskell in the large. ~ Facundo Domínguez. https://www.tweag.io/blog/2023-06-22-lh-assumption-imports/ #Haskell #LiquidHaskell #FunctionalProgramming

Verified causal broadcast with Liquid Haskell. ~ Patrick Redmond, Gan Shen, Niki Vazou, Lindsey Kuper. https://arxiv.org/abs/2206.14767 #Haskell #FunctionalProgramming #LiquidHaskell

Verified causal broadcast with Liquid Haskell. ~ Patrick Redmond, Gan Shen, Niki Vazou, Lindsey Kuper. https://arxiv.org/abs/2206.14767 #Haskell #FunctionalProgramming #LiquidHaskell

I was curious how #LiquidHaskell handles integer overflow, and found this blog entry from 2017: http://ucsd-progsys.github.io/liquidhaskell/blogposts/2017-03-20-arithmetic-overflows.lhs/

Short answer: by default you get the lie that Haskell Ints are unbounded, but you can introduce a bounded numeric typeclass. It would be interesting to try to re-create some smart-contract bugs this way and see if they are caught.

@3j0hn Oh my goodness I actually beat you on part 2 today! I got rank 3090, but I was frustrated that there seemed to be very few opportunities to write good #LiquidHaskell specifications, in part because Set size is not part of the LH specification as things stand today. (I declined to rewrite my depth-first search in a way that would permit a termination proof without it.)

https://github.com/mgritter/aoc-lh/blob/main/2022/day18/Main.hs

@3j0hn Oh my goodness I actually beat you on part 2 today! I got rank 3090, but I was frustrated that there seemed to be very few opportunities to write good #LiquidHaskell specifications, in part because Set size is not part of the LH specification as things stand today. (I declined to rewrite my depth-first search in a way that would permit a termination proof without it.)

https://github.com/mgritter/aoc-lh/blob/main/2022/day18/Main.hs

Starting day 16 of #AdventOfCode using #LiquidHaskell just a few minutes!

https://twitch.tv/markgritter

Starting day 16 of #AdventOfCode using #LiquidHaskell just a few minutes!

https://twitch.tv/markgritter

Halfway done with #AdventOfCode! My live stream coding in #LiquidHaskell starts for day 13... https://www.twitch.tv/markgritter