Scheme Formal Verification
TLA+ bridge for Scheme verification with property-based testing
Daria Pascal
Functional programming, formal methods, and AI systems research
Research Focus
Scheme/Lisp
Building verified functional systems with emphasis on meta-circular evaluation and symbolic computation
Category Theory
Computational approaches to program structure through categorical abstractions and type theory
LLM Integration
AI-powered code analysis and synthesis, bridging symbolic and neural approaches
Formal Verification
TLA+ specifications for real systems with automated property checking
Featured Projects
MIT 6.851 Advanced Data Structures
Functional implementations of advanced data structures from MIT's graduate course
RepoMind
LLM-powered repository analysis and knowledge extraction
Reversible Meta-Synthesis
Inductive program synthesis through reversible computation
Recent Posts
Towards Verified AI: A Functional Programming Approach
Why the convergence of functional programming, formal methods, and AI systems presents unprecedented opportunities for building trustworthy intelligent systems.
Building Verified Systems in Scheme
Exploring the intersection of formal verification and functional programming through TLA+ specifications for Scheme programs.
Category Theory as a Programming Tool
How categorical thinking transforms the way we structure programs, with practical examples in Scheme.