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.