Skip to content

Instantly share code, notes, and snippets.

View jtpaasch's full-sized avatar

JT Paasch jtpaasch

13 followers · 3 following
View GitHub Profile
@jtpaasch
jtpaasch / List_insertion.cpp
Created October 20, 2023 15:51
Working example of the running example on p. 15 of Chang et al, "Shape Analysis," in Trends and Foundations of Programming Languages vol 6, no 1-2, pp. 1-158.
#include <iostream>
using namespace std;
typedef struct list {
struct list * n;
int d;
} list;
void insert(list * l, int d) {
@jtpaasch
jtpaasch / StateMonad.hs
Created October 17, 2023 18:51
Example of Haskell's state monad (after the Monday Morning Haskell blog post)
module Main where
import qualified Control.Monad.State as M
import qualified Data.Array as A
import System.Random (StdGen, mkStdGen, randomR)
-- In a tic-tac-toe game, there is an 'X' player, and an 'O' player
data Player = PlayerO | PlayerX deriving (Eq, Show)
@jtpaasch
jtpaasch / Sexp_parser.hs
Created October 9, 2023 16:29
Parsing S-expressions in Haskell (using S-Cargot)
module Main where
import qualified Data.Text as T
import qualified Text.Parsec.Pos as P
import qualified Data.SCargot as S
import qualified Data.SCargot.Common as C
import qualified Data.SCargot.Language.Basic as B
import qualified Data.SCargot.Repr.WellFormed as W
type Sexp = W.WellFormedExpr (C.Located T.Text)
@jtpaasch
jtpaasch / Fold_left_vs_right.hs
Created October 6, 2023 14:17
The difference between fold left and fold right
-- This version of fold applies 'f' to the head of the list '[a]'
-- to get a new accumulation 'acc', then it recurses into the tail
-- of the list '[a]' where it then repeats. This means that the
-- accumulated results are built up by adding in the elements
-- of the list, one at a time, starting with the first element
-- (on the left), and then moving through them, going right.
foldLeft :: (b -> a -> b) -> b -> [a] -> b
foldLeft f acc xs =
case xs of
[] -> acc
@jtpaasch
jtpaasch / loader.js
Created May 1, 2012 15:07
Javascript module for loading scripts asynchronously.
/**
* A module for loading scripts asynchronously in most browsers.
*
* Note: this module uses the script.async attribute (see line 30), which
* tells the browser to load the script asynchronously. Most modern browsers
* support this async functionality, but those that don't will simply
* overlook it without causing problems.
*
* In addition, older versions of IE, Webkit, and Firefox 4+ that don't
* support the async attribute will still load scripts asynchronously
@jtpaasch
jtpaasch / Sequence_Tutorial_for_Jane_Street_Core.md
Created August 16, 2018 17:05
Tutorial/cheat sheet for using Jane Street Core's Sequences.

Sequence (from Jane Street Core)

Suppose you have a list.

let x = ["a"; "b"; "c"];;

Convert it to a sequence:

@jtpaasch
jtpaasch / Option_tutorial_for_Jane_Street_Core.md
Last active January 22, 2023 05:48
Tutorial/cheat sheet for Jane Street Core's Option.

Option (from Jane Street Core)

Convert a value to an optional something:

let some_message = Option.some "goodbye";;

Suppose you have some data:

@jtpaasch
jtpaasch / OCaml_Compiling_and_Running.md
Last active December 17, 2022 13:35
Tutorial/cheat sheet for compiling/running OCaml programs.
@jtpaasch
jtpaasch / Relational-program-verification.md
Last active October 27, 2022 20:05
Notes on relational program verification

Relational Verification

Beckert, B. and M. Ulbrich. (2018) "Trends in Relational Program Verification." In I. Schaefer and P. Muller (Eds.), Principled Software Development: Essays Dedicated to Arnd Poetzsch-Heffter on the Occasion of His 60th Birthday. Springer, pp. 41-58.

Relational verification verifies relational properties that relate different programs.

To verify relational properties, one must (in principle) compare several runs of the same program.

Some examples of relational properties:

@jtpaasch
jtpaasch / Specification-Synthesis-Notes.md
Last active October 11, 2022 16:22
Some notes on literature on spec synthesis.