Skip to content

Instantly share code, notes, and snippets.

Avatar

Brendan Zabarauskas brendanzab

View GitHub Profile
@gelisam
gelisam / CategorySolver.agda
Created Apr 5, 2021
Automatically generating proofs which only involve associativity of composition and adding/removing identity morphisms.
View CategorySolver.agda
-- Yet another technique for generating proofs in Agda (in addition to the ones
-- I've described in https://gist.github.com/gelisam/486d4992c0f3a3f3da2f58ff0e1a3e72):
-- transform the proposition into a simpler one which can be proved using refl.
--
-- This is the approach I use in my https://github.com/agda/agda-finite-prover
-- package, which can prove equations universally-quantified over finite types,
-- e.g. proving the commutativity of the boolean function '∧'. I simplify the
-- proposition to a long enumeration of all the concrete cases, each of which
-- can be proved using refl:
--
View typelevel-deBruijn-scala
object DeBruijn {
sealed trait Nat
sealed trait Z extends Nat
sealed trait S[n <: Nat] extends Nat
sealed trait Fin[n <: Nat]
case class FZ[n <: Nat]() extends Fin[S[n]]
case class FS[n <: Nat](n : Fin[n]) extends Fin[S[n]]
val here : Fin[S[S[Z]]] = FZ()
@philzook58
philzook58 / z3_tut.v
Created Feb 27, 2021
Z3 Tutorial to Coq
View z3_tut.v
(*|
I had a fun time giving a Z3 tutorial at Formal Methods for the Informal Engineer (FMIE) https://fmie2021.github.io/ (videos coming soon hopefully!). I got to be kind of the "fun dad" with the Z3 tutorial https://github.com/philzook58/z3_tutorial , while at times it felt a bit like Cody's Coq tutorial https://github.com/codyroux/broad-coq-tutorial was trying to feed the kids their vegetables. He knew it was going to be like this from the outset and had a fun little analogy of me downhill skiing while he was about to go on a cross country slog.
There are a number of factors to this.
* I could use Z3's python bindings giving an air of familiarity, whereas everything was incredibly foreign in Coq.
* Z3 can actually be used to declaratively state problems and automatically calculate solutions to them with very little user help, which gives it a lot more "Wow" factor.
* Coq is a tool that requires significantly more background to even comprehend what the hell it is. I still think many aspects of it are tota
View LambdaCubeIn100Lines.hs
-- Based on: http://augustss.blogspot.com/2007/10/simpler-easier-in-recent-paper-simply.html
import Data.List (delete, union)
{- HLINT ignore "Eta reduce" -}
-- File mnemonics:
-- env = typing environment
-- vid = variable identifier in Bind or Var
-- br = binder variant (Lambda or Pi)
-- xyzTyp = type of xyz
-- body = body of Lambda or Pi abstraction
@ekmett
ekmett / IndicesAndLevels.hs
Last active Apr 28, 2021
a pragmatic mix of de bruijn indices and levels
View IndicesAndLevels.hs
{-# language PolyKinds #-}
{-# language BlockArguments #-}
{-# language AllowAmbiguousTypes #-}
{-# language StrictData #-}
{-# language DerivingStrategies #-}
{-# language GeneralizedNewtypeDeriving #-}
{-# language TypeApplications #-}
{-# language BangPatterns #-}
{-# language NPlusKPatterns #-}
{-# language TypeFamilies #-}
@Boarders
Boarders / Comp.agda
Last active Nov 30, 2020
compiler correctness for addition language
View Comp.agda
module Comp where
open import Data.List
using (List; []; _∷_; _++_)
open import Relation.Binary.PropositionalEquality
using (_≡_; refl)
open import Data.Nat
using (ℕ; _+_)
open import Data.List.Properties
using (++-assoc; ++-identityʳ)
@Jack-Works
Jack-Works / 2018.js
Last active May 4, 2021
cRAzY eSnEXt (*all* proposals mixed in)
View 2018.js
#! Aaaaaaaaaaa this is JS!!!
// https://github.com/tc39/proposal-hashbang
// This file is mixing all new syntaxes in the proposal in one file without considering syntax conflict or correct runtime semantics
// Enjoy!!!
// Created at Nov 23, 2018
for await(const x of (new A // https://github.com/tc39/proposal-pipeline-operator
|> do { // https://github.com/tc39/proposal-do-expressions
case(?) { // https://github.com/tc39/proposal-pattern-matching
when {val}: class {
@mb64
mb64 / flat_tree.c
Created Oct 31, 2020
Flat trees in ATS and C
View flat_tree.c
/* A flat representation of
* data Tree = Leaf Int | Node Tree Tree
*
* Either:
* - *ft is LEAF and a single int follows
* - *ft is NODE and two subtrees follow
*/
#define LEAF 0
#define NODE 1
View hattifatteners.awk
#!/usr/bin/awk -f
function hoop(h, w) {
printf("l 0 %d ", -h);
printf("c 0 -%u, %u -%u, %u 0 ", w, w, w, w);
printf("l 0 %d", +h);
}
function hand(x, h, o, l) {
printf("<g transform='translate(%d.5 %d)'>\n", x, h);
@dvanhorn
dvanhorn / syntax-rules-eval.rkt
Last active Oct 25, 2020
A CPS interpreter for a CBV language w/ some fancy features written in syntax-rules
View syntax-rules-eval.rkt
#lang racket
;; A CPS interpreter for a CBV language written in syntax-rules
;; e ::= 'd literal
;; | x variable
;; | (e e ...) application
;; | (λ (x ...) e) abstraction
;; | (let ((x e) ...) e) let
;; | (if e e e) conditional