intro to agda siek

Certainty by Construction Maguire book

Stump Agda book agda2hs blog post jasper

Martin Escardo Introduction to Univalent Foundations of Mathematics with Agda

agda wiki

Agda manual

Programming Language Foundations in Agda

apt-get install agda agda-mode agda-stdlib
echo 'module hello-world where

open import Agda.Builtin.IO using (IO)
open import Agda.Builtin.Unit using (⊤)
open import Agda.Builtin.String using (String)

postulate putStrLn : String → IO ⊤
{-# FOREIGN GHC import qualified Data.Text as T #-}
{-# COMPILE GHC putStrLn = putStrLn . T.unpack #-}

main : IO ⊤
main = putStrLn "Hello world!"

' > /tmp/hello-world.agda
cd /tmp # Why do I have to do this? Me dunno.
agda --compile /tmp/hello-world.agda
agda --help

The hott game Cubical Agda: a cold Introduction sandy maguire book Formalizing category theory in Agda
System F in Agda, for Fun and Profit Algebraic Effects Meet Hoare Logic in Cubical Agda - Kidney, Yang, Wu Timely Computation Conal Elliot Shallowly Embedding Type Theories as Presheaf Models in Agda Frex: dependently-typed algebraic simplification cs 410 mcbride agda abstract bnding trees siek

Well Typed Syntax Formal Metatheory of Second-Order Abstract Syntax Generic Description of Well-Scoped, Well-Typed Syntaxes Erdi 2012 benton et al Strongly Typed Term Representations in Coq

Altenkirch and Reus [1999] Monadic presentations of lambda terms using generalized inductive types

Richard S. Bird and Ross Paterson. 1999. de Bruijn notation as a nested datatype

Allais, Atkey, Chapman, McBride, and McKinna [2021] A type and scope safe universe of syntaxes with binding: their semantics and proofs 2005 mcbride Type-Preserving Renaming and Substitution horsten Altenkirch: How to define type theories?

mcbride thinning and substitution well typed interpeter example idris well typed interpreter lean Stitch: The Sound Type-Indexed Type Checker (Functional Pearl) - eisenberg An algerbaic approahc to typchecking and elaboration - bob atkey Scoped and Typed Staging by Evaluation . two level type theory embedded in agda allais. all sorts of great stuff

Idris recusion schemes in idris

Eh, they’re similar enough. Wow. Idris. Takes me back

Idris 2: Quantitative Type Theory in Practice idris 2 course Seamless, Correct, and Generic Programming over Serialised Data

echo '--re
module Main

main : IO ()
main = putStrLn "Hello world"

x : Int
x = 94

foo : String
foo = "Sausage machine"

--bar : Char
--bar = 

quux : Bool
quux = False

data Tree = Leaf | Node Tree Bits8 Tree
sum : Tree -> Nat
sum t = case t of
    Leaf => 0
    Node l b r =>
        let m = sum l
            n = sum r
        in (m + cast b + n)

q : Nat
q = S Z
y = [1,2,3]

-- import Data.Vect
data Vect : Nat -> Type -> Type where
    VNil : Vect Z a
    VCons : a -> Vect n a -> Vect (S n) a
' > /tmp/test.idr
cd /tmp
idris2 -c  test.idr advent of code 2023

echo "
--re idris2

main : IO ()
main = printLn 42

" > /tmp/test.idr
cd /tmp
idris2  -x main test.idr

Use pack?

Zanzi Lambda Calculus And Bicartesian Closed Categories Second Order Algebraic Theories “two theories” kappa and zeta calculus

Typed Syntax. Thinnings telescope

Relative monads

Quantitative type theory 0 1 omega algebraic paths optics open games Grothendieckconstruction.idr freesemiring.idr brent yorgey theis COMBINATORIAL SPECIES AND LABELLED STRUCTURES phil freeman. Stack safe traversal via dissections zipperized algorithm W more n phd thesis dybjer inductive families type theory as a language workbench

elimination with a motive

fording - mcbride’s thesis. removing indices by adding equations. Kind of like that why of modelling gadts with internal equality constraints? “Elimination with a motive is about two things Fording on the fly. So “black” becomes “any colour you like as long as it’s black”; Maximising the strength of inductive hypotheses in a situation where lexicographic recursion is our expected mode of operation.”

once again indices vs parameters rears its head Two tricks to trivialize higher-indexed families Frex: indexing modulo equations with free extensions

Conor McBride, Ornamental algebras, algebraic ornaments the type

Maybe mcbride works metnally in dependently typed emtatheory