I'm a software engineer in Greece, mostly exploring functional programming, type systems, developer tools, and small libraries that make programming feel more precise and expressive. Recently, my focus has been on Lean, dependent typing, and metaprogramming, building on extensive past experience with F#, C#, and Idris.
- Recently: Lean 4 experiments and typed DSLs
- Previously: extensive work with F#, C#, and Idris
- Higher-kinded programming abstractions
- Algebraic effects and logic programming
- Typed APIs, DSLs, and language experiments
A focused index of my Lean, F#, C#, and Idris work.
- 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
- GitHub: @palladin
- Twitter: @NickPalladinos