Automated code reviews via mutation testing - semantic code coverage.

coverage driven random testing framework

Plutus Groth validator library

Uniswap arbitrage problem analysis

Abstract State Machine Language

LeanSSR: an SSReflect-Like Tactic Language for Lean

Language based on Rewriting Logic

Operational semantics, Type-based information flow security, Hoare logic, Verification conditions, and Separation logic in Agda for the IMP language

Deciding Presburger arithmetic in agda

The ASM Workbench

Merge sort correctness proof

Run GHCi from within a Reflex FRP application and interact with it using a functional reactive interface.

Issue tracker for Hackage maintainance and trustee operations

SMT Based Verification in Haskell. Express properties about Haskell programs and automatically prove them using SMT solvers.

papers of Per Martin Löf

The repository containing the artifact accompanying the paper

A Direct-to-Driver open mobility platform powering the next-generation of mobility applications in India.

A tiny tool that takes output of `htmlize` and turns it into a markdown text consumable by `pandoc`

Experiments with effect systems

TODO

Formal semantics in Agda.

A library for doing generic programming in Agda

An Ugly, untested and mostly unsatifying translator from λProlog code to Latex inference rules

My portfolio contains a lexer generator, a parser generator, my own λProlog interpreter, and several meta-theorems for the propositional logic with their proofs written in Coq.

multi-logic proof generator