[Agda] agda-ocaml - experimental backend

Apostolis Xekoukoulotakis apostolis.xekoukoulotakis at gmail.com
Mon Nov 5 22:43:58 CET 2018


agda-ocaml is an experimental OCaml backend that uses Stephen Dolan's
malfunction package to target OCaml's internal flambda representation. It
is an extension of previous work by Frederik Hanghøj Iversen and Jan Mas
Rovira.

The main features of this version is that it supports pragmas. You can use
OCaml from Agda or export agda code as an OCaml module.

The internal representation of agda mimics the internal representation of
OCaml, so that any OCaml data type or function is easily accessible from
Agda and the opposite.

If you are interested in testing it, I managed to write some documentation
in its github repository as well as its current limitations.

https://github.com/xekoukou/agda-ocaml
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20181105/ddfe5d28/attachment.html>


More information about the Agda mailing list