Pinned Repositories
ditto
A Super Kawaii Dependently Typed Programming Language
cry
A CommonLisp CLOS-like parse tree library for Ruby... read (and write) it and weep.
dataflow
Dataflow concurrency for Ruby (inspired by the Oz language)
dtgp
Dependently Typed Genetic Programming
generic-elim
Source code accompanying the paper "Generic Constructors and Eliminators from Descriptions"
generic-reuse
Source code accompanying the draft paper "Generic Zero-Cost Reuse for Dependent Types"
infir
Source code accompanying the paper "Generic Lookup and Update for Infinitary Inductive-Recursive Types"
Lemmachine
REST'ful web framework in Agda
leveling-up
Source code accompanying the paper "Leveling Up Dependent Types"
sbe
Accompanying source code for technical report "Hereditary Substitution by Canonical Evaluation (SbE)".
larrytheliquid's Repositories
larrytheliquid/leveling-up
Source code accompanying the paper "Leveling Up Dependent Types"
larrytheliquid/generic-elim
Source code accompanying the paper "Generic Constructors and Eliminators from Descriptions"
larrytheliquid/linear-temporal-logic
sandbox for playing with linear temporal logic
larrytheliquid/spire
The Spire Programming Language
larrytheliquid/generic-reuse
Source code accompanying the draft paper "Generic Zero-Cost Reuse for Dependent Types"
larrytheliquid/zero-cost-coercions
Source code accompanying the draft paper "Zero-Cost Coercions for Program and Proof Reuse"
larrytheliquid/mltt-lecture
larrytheliquid/plclub-expless
PL Club talk on Expressionless Weak-Head Normal Forms
larrytheliquid/sbe
Accompanying source code for technical report "Hereditary Substitution by Canonical Evaluation (SbE)".
larrytheliquid/thesis
larrytheliquid/buffer-overflows
larrytheliquid/expless
Adaptation of Ch. 4 of James Chapman's thesis to Values and Hereditary Substitution (note to self: currently missing some theorems still on laptop)
larrytheliquid/plclub-apr-2013
Code for a PL Club I gave at PSU on April 19, 2013.
larrytheliquid/plclub-oct-2012
Code for a PL Club I gave at PSU on October 26, 2012
larrytheliquid/quickcheck-state-machine
Test monadic programs using state machine based models
larrytheliquid/infir
Source code accompanying the paper "Generic Lookup and Update for Infinitary Inductive-Recursive Types"
larrytheliquid/aaip11
LaTeX source for paper "Verified Stack-Based Genetic Programming via Dependent Types".
larrytheliquid/agda
Agda is a dependently typed programming language / interactive theorem prover.
larrytheliquid/agda-stdlib
The Agda standard library
larrytheliquid/foo-tester
just a test - ignore
larrytheliquid/gpcl
Genetic Programming using Combinatory Logic
larrytheliquid/hash-cons
Experimenting with savings on hash-cons'ing Desc-based definitions
larrytheliquid/hs-rqlite
An unofficial Haskell client for RQlite
larrytheliquid/Idris-dev
A Dependently Typed Functional Programming Language
larrytheliquid/idris-tutorial
A tutorial to the Idris Programming Language.
larrytheliquid/jekyll-multiverse-template
HTML5UP's Multiverse theme for Jekyll
larrytheliquid/mathlog
CS 510 - Mathematical Logic and Programming Languages
larrytheliquid/resume
Personal Resume
larrytheliquid/rpe
Code for PSU's Research Proficiency Exam (RPE)
larrytheliquid/site
Personal Website