Skip to content

Instantly share code, notes, and snippets.

Avatar

KC Sivaramakrishnan kayceesrk

View GitHub Profile
@kayceesrk
kayceesrk / stlc.prolog
Last active Nov 22, 2019
Type inference and program synthesis from simply typed lambda calculus type checking rules
View stlc.prolog
?- set_prolog_flag(occurs_check,true).
lookup([(X,A)|_],X,A).
lookup([(Y,_)|T],X,A) :- \+ X = Y, lookup(T,X,A).
/* Rules from the STLC lecture */
pred(D,DD) :- D >= 0, DD is D - 1.
type(_,u,unit,D) :- pred(D,_).
@kayceesrk
kayceesrk / Dockerfile
Created Feb 26, 2019
Dockerfile for installing irmin-unix
View Dockerfile
From ocaml/opam2
RUN sudo apt update
RUN sudo apt install -y m4 perl libgmp-dev pkg-config
RUN opam remote add upstream https://opam.ocaml.org && \
opam update && opam upgrade
RUN git clone https://github.com/mirage/irmin
WORKDIR irmin
RUN opam pin add -k git -n irmin . && \
opam pin add -k git -n irmin-unix . && \
opam pin add -k git -n irmin-fs . && \
View pldi18_aec_ldrf.md

Artefact Evalution for "Bounding Data Races in Space and Time"

This document contains instructions for the artefact evaluation. The draft paper is available at kcsrk.info/papers/pldi18-memory.pdf.

Access to benchmarking machines

The main evaluation in the paper is the overhead of compiling our proposed memory model to relaxed architectures such as ARM and POWER (Fig 7 on page 10).

View reverse_mode_ad.ml
(* Reverse-mode algorithmic differentiation using effect handlers.
Adapted from https://twitter.com/tiarkrompf/status/963314799521222656.
See https://openreview.net/forum?id=SJxJtYkPG for more information. *)
module F = struct
type t = { v : float; mutable d : float }
let mk v = {v; d = 0.0}
effect Plus : t * t -> t
@kayceesrk
kayceesrk / gcstress.ml
Created Aug 26, 2017
OCaml multicore GC stress test
View gcstress.ml
(* GC stress/performance test.
Uses only core GC features - no finalisers, weak references, etc. *)
type work = F : (int -> 'a) * ('a -> int) -> work
type bintree = Leaf of int | Branch of bintree * bintree
let tree =
let rec mktree = function
| 0 -> Leaf 1
| n -> Branch (mktree (n-1), mktree (n-1)) in
View eff.ml
(* Requires: OCaml 4.03.0+ *)
(* Usage: `ocaml eff.ml` *)
(** Identifiers *)
module Ident = struct
type t = string
let id = ref 0
let create base =
View st_posix.h
/***********************************************************************/
/* */
/* OCaml */
/* */
/* Xavier Leroy and Damien Doligez, INRIA Rocquencourt */
/* */
/* Copyright 2009 Institut National de Recherche en Informatique et */
/* en Automatique. All rights reserved. This file is distributed */
/* under the terms of the GNU Library General Public License, with */
/* the special exception on linking described in file ../../LICENSE. */
View handler_monad.ml
module type Handler = sig
type effect = ..
type 'a t
type cont
val return : 'a -> 'a t
val (>>=) : 'a t -> ('a -> 'b t) -> 'b t
val run : unit t -> unit
val handle : 'a t -> (effect -> cont -> unit t) -> unit t
val continue : cont -> unit t
View Dockerfile
## Docker file for OCaml with GDB support
#
# Build
# -----
# $ mkdir monda-docker
# $ cp <this_file> monda-docker/
# $ docker build --force-rm=true -t monda .
# ..takes a while..
#
# Run
View Dockerfile
## Docker file for OCaml with GDB support
#
# Build
# -----
# $ mkdir monda-docker
# $ cp <this_file> monda-docker/
# $ docker build --force-rm=true -t monda .
# ..takes a while..
#
# Run
You can’t perform that action at this time.