Using FFI’s pragmas in Agda
Andrés Eugenio Castaño Cardenas
acastan (at) eafit (dot) edu (dot) co
June 20, 2011
Abstract:
This paper exhibits the power that Agda can have besides all the capability of programming with
dependent types, Agda is a proof assistant, it is an interactive system for writing and checking
proofs, that so named interactivity is seen from an other point
of view, the capability of interact with an Agda program,
the option that we used to achieve this goal for writing interactive
programs is the foreign function interface a way of calling Haskell functions from
Agda.
