An OCaml Backend for Agda with Malfunctional Programming

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.

Related content:

Related Posts

Author | Gemma Gordon

Gemma is the Operations Director for the OCaml Labs group in the Cambridge Computer Laboratory, and covers day-to-day management, investigates funding opportunities and organises events.