Skip to content

Instantly share code, notes, and snippets.

View siraben's full-sized avatar

Ben Siraphob siraben

View GitHub Profile
@siraben
siraben / rk4.nix
Last active April 7, 2023 21:11
Implementation of sine function in Nix using fourth-order Runge-Kutta
{ lib ? (import <nixpkgs> {}).lib }:
with lib;
let
# Fourth-order Runge-Kutta method
rk4 = f: x0: y0: z0: h:
let
k1_y = z0;
k1_z = f x0 y0 z0;
@siraben
siraben / owner.sol
Created November 6, 2022 22:54
Example Solidity contract with an owner field
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.7.0 <0.9.0;
/**
* @title Owner
* @dev Set & change owner
*/
contract Owner {
@siraben
siraben / factorial.txt
Last active September 25, 2022 18:32
Recursive descent parsing in Cool
((\f. (\x. (f \v. ((x x) v)) \x. (f \v. ((x x) v))) \r. \n. i(n,o,m(n,(r d(n))))) x)
@siraben
siraben / cbv.cl
Created September 8, 2022 18:52
Call-by-value λ-calculus interpreter in Cool
-- Call-by-value lambda calculus in cool
(*
data Expr = Var Str
| Abs Str Expr
| App Expr Expr
| Sub1 Expr
| Mul Expr Expr
| Add Expr Expr
| Ifz Expr Expr Expr
*)
@siraben
siraben / Proving insertion sort in Coq.pdf
Last active July 13, 2022 01:50
Proving insertion sort correct easily in Coq
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverlappingInstances #-}
{-# LANGUAGE TypeOperators #-}
module ExtALaCarte where
@siraben
siraben / vandy_covid.ipynb
Last active February 22, 2022 16:25
Web scraping Vanderbilt's COVID-19 dashboard
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
@siraben
siraben / no_surject_12.v
Last active December 17, 2021 23:20
Constructive proof that there are no surjections from {1} to {1,2}
(* There are no surjections from {1} to {1,2} *)
Definition surjective {A B} (f : A -> B) := forall (b : B), exists (a : A), b = f a.
Definition One := unit.
Definition Two := bool.
Theorem no_surject_one_two : ~ exists (f : One -> Two), surjective f.
Proof.
@siraben
siraben / countable_choice_wikipedia.v
Created August 2, 2021 17:10
"countable choice" according to wikipedia
(* P is a family of nat-indexed sets of nat such that:
H: for all n, there is an m such that m ∈ P n
-----------
Then we show that there is a choice function f
*)
Theorem countable_choice_wikipedia
(P : nat -> (nat -> Prop)) (H : forall n, { m | P n m }) : { f | forall n, (exists m, P n m /\ f n = m)}.
Proof.
set (f := fun (n : nat) => let (m, Hm) := H n in m).
exists f.
@siraben
siraben / futamura.v
Last active July 17, 2021 08:57
Futamura Projections in Coq
Require Import ssreflect ssrfun.
Module Futamura.
(* Program from a -> b written in L *)
Inductive Program {a b language : Type} :=
| mkProgram : (a -> b) -> Program.
Definition runProgram {A B L} (p : @Program A B L) := match p with mkProgram f => f end.
Notation "[ S | a >> b ]" := (@Program a b S) (at level 2) : type_scope.