Ilya Sergey

pnp. Lecture notes for a short course on proving/programming in Coq via SSReflect.

reachability. Experimental implementation of k-CFA and Pushdown k-CFA with optional Abstract Garbage Collection for LambdaJS and a subset of Scheme programming language

monadic-cfa. Generic implementation of different CFA families based on monadic decomposition

plt-redex-fj. A PLT Redex implementation of Featherweight Java

scilla-demo. Scilla Examples and Exercises

YSC2229. Introductory Data Structures and Algorithms

semantic-slicer. Slicing programs to decompose them into independent procedures

GHC-XAppFix. Extension of Glasgow Haskell Compiler to support recursive applicative bindings

typechecker-transformations. An implementation of the mechanical correspondence between algorithms for type checking

scilla-benchmarks. Benchmarking suite for testing the performance of Scilla against EVM

coq-exercises. Exercises for Coq course, based on SSReflect, Coq'Art and CPDT

funind. Coq

uplcg. Untitled PL Card Game

GHC-XAppFix-BaseLibrary. Augmented base library for GHC for ApplicativeFix support

Gradual-Ownership. Experimental implementation of Gradual Ownership Types for Java 1.4

GHC-XAppFix-TestSuite. Tests for ApplicativeFix GHC extension

geometry-testing. Geometry Generation and Testing Framework

htt. Hoare Type Theory

YSC4231. Parallel, Concurrent and Distributed Programming