Agate–an Agda-to-Haskell compiler Export

@article{citeulike:2968696, abstract = {We report some features of Agate, a compiler for the dependently typed functional language of Agda proof-assistant. Agate is developed to be an experimental platform for practice of dependently typed programming and it extends Agda language with I/O facilities and calls to Haskell functions. The first feature is the use of higher order abstract syntax to translate terms of Agda language into untyped λ-calculus encoded in Haskell. The second is the application of Haskell class mechanism to embed typed Haskell terms in the universal type for untyped λ-calculus. This approach makes Agate very lightweight. Performance report of some codes emitted by Agate is given.}, author = {Ozaki, Hiroyuki and Takeyama, Makoto and Kinoshita, Yoshiki}, citeulike-article-id = {2968696}, day = {5}, keywords = {2006, agda, compiler, haskell, transformation}, month = {October}, posted-at = {2008-07-07 09:39:22}, priority = {2}, title = {Agate–an Agda-to-Haskell compiler}, year = {2006} }

TY - JOUR ID - citeulike:2968696 L3 - citeulike-article-id:2968696 N2 - We report some features of Agate, a compiler for the dependently typed functional language of Agda proof-assistant. Agate is developed to be an experimental platform for practice of dependently typed programming and it extends Agda language with I/O facilities and calls to Haskell functions. The first feature is the use of higher order abstract syntax to translate terms of Agda language into untyped λ-calculus encoded in Haskell. The second is the application of Haskell class mechanism to embed typed Haskell terms in the universal type for untyped λ-calculus. This approach makes Agate very lightweight. Performance report of some codes emitted by Agate is given. TI - Agate–an Agda-to-Haskell compiler KW - 2006 KW - agda KW - compiler KW - haskell KW - transformation AU - Ozaki, Hiroyuki AU - Takeyama, Makoto AU - Kinoshita, Yoshiki PY - 2006/10/05/ ER -