The experimental backend for Agda targets the OCaml compiler via Malfunction - a library created by OCaml Labs’ own Stephen Dolan. Malfunction is a compilation target that allows functional programming languages to take advantage of the OCaml flambda optimisations, efficient runtime and garbage collector.
Agda is an open-source, dependently typed programming language and proof assistant. With a basis in intuitionistic type theory, it has many similarities with OCaml, and provides the added functionality of constructive logic: a proposition is proved by writing a program of the corresponding type.
- Multicore OCaml ARM64 Backend
- Cambio, OCaml and Karaoke at the MirageOS Marrakech Hack Retreat 2017
- Using Menhir to Build Grammar Attributes
- OCaml 4.04.1 Released
- Parsing the Email Standard with TypeBeat
- Databox Open-Source Software Community Launch
- Composable Builds for OCaml with Jbuilder
- MirageOS Hack Updates
- Algebraic Subtyping: PhD thesis
- Databox Launch Event: 24th March, Cambridge