I'm a PL hacker interested in applying theory and research ideas to practical programming. I work mostly through functional programming, dependent typing, and metaprogramming, building tools and libraries that make programming feel more precise and expressive.
- Stream fusion and data-processing libraries
- Distributed and parallel programming
- Programming with effects and handlers
- DSLs for logic programming and SMT solvers
- DBLP profile - Stream fusion, practical libraries for OCaml and Scala, and formalization work in Agda
- lean-reducers - Parallel, fused reducers for Lean 4 with Task-backed chunked folds and law-aware combiners
- lean-eff - Lean 4 extensible effects with concrete rows, handlers, and practical examples
- lean-bitsyntax - Lean 4 bit syntax experiment
- SmtLibDsl - Type-safe SMT-LIB DSL for Lean 4 with Z3 integration
- lean-snippets - Lean 4 snippets
- Higher - Higher-kinded programming in F#
- Eff - Algebraic effects in F#
- logic - Logic programming for F#
- fsharp-snippets - F# snippets and examples
- Delimcc - Multi-prompt delimited control in F#
- Streams - Functional-style pipelines for streams of data
- LinqOptimizer - Query optimizer/compiler for LINQ
- multi-stage-fsharp - Multi-stage programming in F#
- MBrace.Core - Core MBrace programming model and runtime
- GpuLinq - GPGPU programming through OpenCL and LINQ
- TypedSqlBuilder - Type-safe SQL expression builder DSL
- EffSharp - Effects and handlers in C#
- Splicer - Expression tree splicing in C#
- idris-snippets - Idris snippets and experiments