Suppose we are working with the following Liquid Haskell code:
{-@ LIQUID "--ple" @-}
{-@ LIQUID "--reflection" @-}
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
/ 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
| nix-shell -p "python3.withPackages (ps: with ps; [ dbus-python distro ])" --run "python3 <your-eduroam.py>" |
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" @-} |
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
/ 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 |
OlderNewer