An Agda mechanization of the Streamlet consensus protocol.

replication of "Certified Symbolic Management of Multi-party Financial Contracts" https://github.com/HIPERFIT/contracts

Formal specifications of the Cardano ledger

AGDA formal verification experiments.

Marlowe interpreter and contract manager

My honours project (with thesis), submitted in completion of the BSc Combined Honours in Mathematics & Computer Science at Dalhousie University in April 2022.

The agda-unimath library

Agda is a dependently typed programming language / interactive theorem prover.

Compiling Agda code to readable Haskell

Key Information Document, implementation of the calculations in the annexes

Implementation of the ACTUS taxonomy

Key Information Document generation

Key Information Document, implementation of the RTS of the PRIIPs regulation

Programming language for literate programming law specification

Marlowe language specification

Domain specific language for financial contracts

Writing financial contracts in Julia

Haskell embedding of PlusCal

Advent of Code 2021 in Futhark

Extracting Futhark code from the Coq proof assistant

The Plutus language implementation and tools

This is a fork of the IOHK Plutus Pioneer Program repository. I am adding READMEs to each of the lectures to transcribe the audio.

Formal verification of the Algorand consensus protocol

High-performance TensorFlow library for quantitative finance.

Brainfuck formalized in Coq

An introduction to programming language theory in Agda

The Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environmen…

A framework for smart contract verification in Coq

Prototype implementation of domain-specific language for the design of smart-contracts over cryptocurrencies