Skip to content

Instantly share code, notes, and snippets.

View jonsterling's full-sized avatar

Jon Sterling jonsterling

View GitHub Profile
@jonsterling
jonsterling / exists.ml
Created March 17, 2016 15:14
existential quantifier in OCaml
(* an abstract signature for instantiations of the existential quantifier *)
module type EXISTS =
sig
(* the predicate *)
type 'a phi
(* the existential type *)
type t
(* the introduction rule *)
@jonsterling
jonsterling / STC.agda
Created February 26, 2021 02:54
STC.agda
{-# OPTIONS --type-in-type --cubical --rewriting --confluence-check #-}
module stc-playground where
open import Cubical.Foundations.Prelude
open import Agda.Builtin.Equality renaming (_≡_ to _≣_)
open import Agda.Builtin.Equality.Rewrite
open import Agda.Primitive
\RequirePackage{expl3}
\RequirePackage{xparse}
\ProvidesExplPackage {namespace} {2020/08/31} {0.1} {Compositional namespaces for labels}
\tl_new:N \l_ns_stk
\cs_new:Npn \ns_push:n #1 {
\tl_put_right:Nn \l_ns_stk {#1}
\tl_put_right:Nn \l_ns_stk {/}
@jonsterling
jonsterling / GluedEval.hs
Created May 8, 2020 16:44 — forked from AndrasKovacs/GluedEval.hs
Non-deterministic normalization-by-evaluation in Olle Fredrikkson's flavor.
{-# language Strict, LambdaCase, BlockArguments #-}
{-# options_ghc -Wincomplete-patterns #-}
{-
Minimal demo of "glued" evaluation in the style of Olle Fredriksson:
https://github.com/ollef/sixty
The main idea is that during elaboration, we need different evaluation
\RequirePackage{expl3}
\RequirePackage{xparse}
\RequirePackage{ebproof}
%% This package is an extension and modification of code by Emmanuel Beffara
\ExplSyntaxOn
\cs_new_protected:Npn \__formulas_split: {
$\hskip 1em plus 1fil$\displaystyle
\section{Focused Sequent Calculus}
Focused sequent calculus has several class of proposition\footnote{We are
writing $\Neg{a},\Pos{a}$ for negative and positive atoms respectively. You may
also see these written as $\Neg{P},\Pos{P}$.} and context. We summarize them
below, noting that $\Pos{\Omega}$ ranges over ordered lists, whereas $\Gamma$
ranges over multisets:
\begin{grammar}
negative & \Neg{A} &
%!TEX TS-program = xelatex
%!TEX encoding = UTF-8 Unicode
\documentclass[letterpaper, 12pt]{article}
\usepackage{amsmath,amsfonts,amssymb,fontspec}
\defaultfontfeatures{Mapping=tex-text}
\setmainfont{Adobe Caslon Pro}
\title{\Large\sc title goes here}
\author{Jonathan M. Sterling}
Core RedML is (so far) a one-sided, polarized L calculus in the style of Curien-Herbelin-Munch.
Lambda calculus can be compiled to Core RedML through a bunch of gnarly macros. For instance, the term
(((lam [x] (lam [y] (pair x y))) nil) nil)
should evaluate to a pair of nils. This term is compiled into Core RedML as the first stage of the following
computation trace, which shows how it computes to the desired pair.
State: (cut
Flat profile:
Each sample counts as 0.01 seconds.
% cumulative self self total
time seconds seconds calls ms/call ms/call name
25.18 1.76 1.76 2415 0.73 0.85 mark_slice
10.44 2.49 0.73 4193520 0.00 0.00 camlHashtbl__insert_bucket_1371
9.87 3.18 0.69 6306936 0.00 0.00 camlHashtbl__add_1385
7.73 3.72 0.54 67916414 0.00 0.00 caml_page_table_lookup
5.87 4.13 0.41 4771 0.09 0.21 caml_empty_minor_heap
var hljs=new function(){var p={};var a={};function n(c){return c.replace(/&/gm,"&amp;").replace(/</gm,"&lt;").replace(/>/gm,"&gt;")}function k(s,r){if(!s){return false}for(var c=0;c<s.length;c++){if(s[c]==r){return true}}return false}function e(s,r,c){var t="m"+(s.cI?"i":"")+(c?"g":"");return new RegExp(r,t)}function j(r){for(var c=0;c<r.childNodes.length;c++){node=r.childNodes[c];if(node.nodeName=="CODE"){return node}if(!(node.nodeType==3&&node.nodeValue.match(/\s+/))){return null}}}function h(u,t){var s="";for(var r=0;r<u.childNodes.length;r++){if(u.childNodes[r].nodeType==3){var c=u.childNodes[r].nodeValue;if(t){c=c.replace(/\n/g,"")}s+=c}else{if(u.childNodes[r].nodeName=="BR"){s+="\n"}else{s+=h(u.childNodes[r])}}}s=s.replace(/\r/g,"\n");return s}function b(t){var r=t.className.split(/\s+/);r=r.concat(t.parentNode.className.split(/\s+/));for(var c=0;c<r.length;c++){var s=r[c].replace(/^language-/,"");if(p[s]||s=="no-highlight"){return s}}}function d(c){var r=[];(function(t,u){for(var s=0;s<t.childNodes.len