Skip to content

Instantly share code, notes, and snippets.


Jonathan Sterling jonsterling

View GitHub Profile
jonsterling / GluedEval.hs
Created May 8, 2020 — forked from AndrasKovacs/GluedEval.hs
Non-deterministic normalization-by-evaluation in Olle Fredrikkson's flavor.
View GluedEval.hs
{-# language Strict, LambdaCase, BlockArguments #-}
{-# options_ghc -Wincomplete-patterns #-}
Minimal demo of "glued" evaluation in the style of Olle Fredriksson:
The main idea is that during elaboration, we need different evaluation
View jon-ebproof.sty
%% This package is an extension and modification of code by Emmanuel Beffara
\cs_new_protected:Npn \__formulas_split: {
$\hskip 1em plus 1fil$\displaystyle
View excerpt.tex
\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:
negative & \Neg{A} &
View gist:6bed2d3327b83d071ab397d290b6e1db
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
View gist:2945940f555a37cc9349e79def330647
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
jonsterling / LabelledAdd1.agda
Created May 13, 2018 — forked from larrytheliquid/LabelledAdd1.agda
Labelled types demo ala "The view from the left" by McBride & McKinna. Labels are a cheap alternative to dependent pattern matching. You can program with eliminators but the type of your goal reflects the dependent pattern match equation that you would have done. Inductive hypotheses are also labeled, and hence you get more type safety from usin…
View LabelledAdd1.agda
open import Data.Nat
open import Data.String
open import Function
open import LabelledTypes
module LabelledAdd1 where
add : (m n : ℕ) "add" ∙ m ∙ n ∙ ε ∶ ℕ ⟩
add m n = elimℕ (λ m' "add" ∙ m' ∙ n ∙ ε ∶ ℕ ⟩)
View new-mlton-results.txt
[0.066684s] Checked test/success/V-types.prl
[0.022747s] Checked test/success/bool-fhcom-without-open-eval.prl
[0.009820s] Checked test/success/bool-pair-test.prl
[0.010696s] Checked test/success/dashes-n-slashes.prl
[0.009144s] Checked test/success/decomposition.prl
[0.006263s] Checked test/success/discrete-types.prl
[0.013531s] Checked test/success/empty.prl
[0.009508s] Checked test/success/equality-elim.prl
[0.017783s] Checked test/success/equality.prl
[0.017168s] Checked test/success/fcom-types.prl
View LOL.v
This file has been truncated, but you can view the full file.
Nuprl_functional =
λ _top_assumption_ : nat,
(λ (_evar_0_ : (λ n : nat, matrix_functional (Nuprl n)) 0)
(_evar_0_0 : ∀ n : nat, (λ n0 : nat, matrix_functional (Nuprl n0)) (S n)),
_top_assumption_ as n
return ((λ n0 : nat, matrix_functional (Nuprl n0)) n)
View recitation-source.tex
\usepackage{amsmath, amssymb, proof, microtype, hyperref}
\usepackage{mathpartir} % for mathpar, not for proofs
View gist:486673f7943f5ddce7c68d2389341f90
module experiment where
open import Agda.Primitive
open import Prelude.List
open import Prelude.Size
open import Prelude.Monoidal
open import Prelude.Monad
open import Prelude.Functor
open import Prelude.Natural
open Size using (∞)
You can’t perform that action at this time.