-
Input Output (IOG)
- Kirkwall, Orkney, Scotland
- https://omelkonian.github.io
- https://orcid.org/0000-0003-2182-2698
- @omelkoni
- @omelkonian@mathstodon.xyz
Highlights
- Pro
-
agda-dependencies Public
An Agda backend for visualizing lemma dependencies.
Haskell MIT License UpdatedNov 4, 2025 -
agda-irrelevance Public
Irrelevance utitilites for the Agda standard library.
Agda MIT License UpdatedOct 14, 2025 -
-
setup-agda Public
Set up your GitHub Actions workflow with a specific version of Agda (+ stdlib + libraries from git repos)
-
-
-
-
agda2train Public
Prototyping an Agda backend to generate training data for machine learning.
-
hoare-ledgers Public
Separation logic for UTXO-based blockchain ledgers
-
agda-minimal-backend Public template
Rustic skeleton for developing a new Agda backend.
-
Agda is a dependently typed programming language / interactive theorem prover.
Haskell Other UpdatedDec 3, 2024 -
europroofnet.github.io Public
Forked from EuroProofNet/europroofnet.github.ioSources of the EuroProofNet web site.
Ruby UpdatedNov 14, 2024 -
formal-utxo Public
Formalization of the UTxO abstract model for (bitcoin-style) blockchain transactions.
-
formal-bitml Public
Formalization of the Bitcoin Modelling Language (BitML).
-
-
formal-prelude Public
Simple extension of Agda's standard library for personal use.
-
-
agda-lenses Public
Rustic lenses library for Agda, equipped with automatic generic deriving.
-
-
-
agda2hs Public
Forked from agda/agda2hsCompiling Agda code to readable Haskell
Agda MIT License UpdatedFeb 26, 2024 -
structured-contracts Public
Playgroup for small-step-style simulation verification of EUTxO smart contracts.
Agda UpdatedFeb 5, 2024 -
formal-ledger-specifications Public
Forked from IntersectMBO/formal-ledger-specificationsFormal specifications of the cardano ledger
Agda Apache License 2.0 UpdatedOct 24, 2023 -
language-rust Public
Forked from harpocrates/language-rustParser and pretty-printer for the Rust language
Haskell BSD 3-Clause "New" or "Revised" License UpdatedSep 18, 2023 -
-
-
formal-dolev-yao Public
Playground for formalizing Dolev-yao models in Agda.
Agda UpdatedJun 2, 2023 -
contract-automata Public
Playground for refinement-style verification of EUTxO smart contracts.
Agda UpdatedNov 23, 2022 -
plfa.github.io Public
Forked from plfa/plfa.github.ioIntroduction to programming language theory in Agda
Agda Creative Commons Attribution 4.0 International UpdatedNov 21, 2022 -