Suppose we are working with the following Liquid Haskell code:
{-@ LIQUID "--ple" @-}
{-@ LIQUID "--reflection" @-}
AlecsFerra
/ install.sh
Created
February 10, 2026 10:08
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| #! /usr/bin/env bash | |
| DIRS=( | |
| "liquid-prelude" | |
| "liquid-parallel" | |
| "liquid-vector" | |
| "." # This must be the last entry | |
| ) | |
| echo "Installing libraries globally..." |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| theory Scratch | |
| imports ZF | |
| begin | |
| consts ty :: "i" | |
| datatype "ty" | |
| = TyNat | |
| | TyBool | |
| | TyArr ("τ ∈ ty", "υ ∈ ty") |
AlecsFerra
/ ExprCompiler.hs
Created
November 22, 2024 15:07
Correct by construction stack compiler in LH
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# LANGUAGE GADTs #-} | |
| {-@ LIQUID "--ple" @-} | |
| {-@ LIQUID "--etabeta" @-} | |
| {-@ LIQUID "--reflection" @-} | |
| {-@ LIQUID "--dependantcase" @-} | |
| module ExprCompiler where | |
| import Language.Haskell.Liquid.ProofCombinators |
AlecsFerra
/ CCDep.hs
Last active
April 29, 2025 13:02
Implementation in LH of Calculating Dependently-Typed Compilers
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| -- Implementation in LH of Calculating Dependently-Typed Compilers | |
| -- https://people.cs.nott.ac.uk/pszgmh/well-typed.pdf | |
| {-# LANGUAGE GADTs #-} | |
| {-# OPTIONS_GHC -fplugin=LiquidHaskell #-} | |
| {-@ LIQUID "--ple" @-} | |
| {-@ LIQUID "--reflection" @-} | |
| {-@ LIQUID "--max-case-expand=4" @-} |
AlecsFerra
/ SKIDC.hs
Last active
November 22, 2024 14:40
Implementation in LH of A correct-by-construction conversion from lambda calculus to combinatory logic
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| // Implementation in LH of A correct-by-construction conversion from lambda calculus to combinatory logic | |
| // https://webspace.science.uu.nl/~swier004/publications/2023-jfp.pdf | |
| {-# Language GADTs #-} | |
| {-@ LIQUID "--reflection" @-} | |
| {-@ LIQUID "--ple" @-} | |
| {-@ LIQUID "--full" @-} | |
| {-@ LIQUID "--max-case-expand=4" @-} | |
| {-@ LIQUID "--etabeta" @-} |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| nix-shell -p "python3.withPackages (ps: with ps; [ dbus-python distro ])" --run "python3 <your-eduroam.py>" |
AlecsFerra
/ flatten.py
Created
June 27, 2024 16:59
Transform a LaTeX project using \import and \subimport in a standalone LaTeX file
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| #! /usr/bin/env python3 | |
| # flatten.py | |
| # Copyright (C) 2024 Alessio Ferrarini <github.com/alecsferra> | |
| # | |
| # This program is free software: you can redistribute it and/or modify | |
| # it under the terms of the GNU General Public License as published by | |
| # the Free Software Foundation, either version 3 of the License, or | |
| # (at your option) any later version. | |
| # |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# LANGUAGE GADTs #-} | |
| {-# LANGUAGE DataKinds #-} | |
| {-# LANGUAGE FunctionalDependencies #-} | |
| {-# LANGUAGE UndecidableInstances #-} | |
| {-# LANGUAGE AllowAmbiguousTypes #-} | |
| import Data.Data (Proxy (Proxy)) | |
| import Data.Kind (Type) | |
| import Text.Printf (printf) |
AlecsFerra
/ AxiomK.agda
Last active
May 20, 2023 19:07
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| module AxiomK where | |
| open import Relation.Binary.PropositionalEquality using (_≡_) | |
| open _≡_ | |
| -- All the equality proofs are the same ⁾ | |
| -- Unless we use the `--without-K` option ⁾ | |
| same-≡ : ∀ {l} {A : Set l} {a b : A} → (p₁ p₂ : a ≡ b) → p₁ ≡ p₂ | |
| same-≡ refl refl = refl |
NewerOlder