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.
- Windows Unicode Support - A Bug-Fix 12 Years in the Making
- Fuzzing for CI Workflows
- Testing Your Own Fork With OCaml's GitHub CI
- Platforms, Packaging, Progress
- Merlin 3.0.0 on Windows
- A New Implementation of Git
- Major Releases of Cohttp, Conduit, DNS and TCP/IP Libraries
- OCaml 4.05.0 Released
- Intel Hyper-Threading Bug Uncovered by OCaml Developers
- Unsigned Integers as Built-In Types or as a Library?