Ascetic Slug
Ascetic Slug
Posts
Publications
About me
Contact
Light
Dark
Automatic
Posts
Using dependent types to write proofs in Haskell
We all know that we can use Haskell to write functional programs that compute stuff. But can we also use Haskell to write mathematical proofs? Yes!
Jan Mas Rovira
Jun 2, 2021
Logic
,
Haskell
Run-length encoding verified in Agda
This post is intended to be a guided exercise (with a proposed solution) for Agda beginner's who are familiar with the basics and want to work on a slightly more involved exercise than proving basic properties about natural numbers.
Sep 7, 2019
Agda
,
Verification
An Agda eDSL for well-typed Hilbert style proofs
I present an Agda eDSL for writing Hilbert style proofs for logic $K$.
Jan Mas Rovira
May 19, 2019
Logic
,
Agda
Ascii fractals
Getting hypnotized by the shape of a fractal is certainly fascinating. In this blog, we will write a Haskell program that creates fractals from a base pattern. The recursive nature of the fractals allow a simple implementation in Haskell.
Jan Mas Rovira
Feb 20, 2018
Haskell
Cite
×