Agate –an Agda-to-Haskell compiler

• OZAKI Hiroyuki

  Research Center for Verification and Semantics (CVS), National Institute of Advanced Industrial Science and Technology (AIST)

• TAKEYAMA Makoto

  Research Center for Verification and Semantics (CVS), National Institute of Advanced Industrial Science and Technology (AIST)

• KINOSHITA Yoshiki

  Research Center for Verification and Semantics (CVS), National Institute of Advanced Industrial Science and Technology (AIST)

Bibliographic Information

Other Title

• Agate(アガテ)–AgdaからHaskellへのコンパイラ

Abstract

We report some features of Agate, a compiler for the dependently typed functional language of the Agda proof-assistant. Agate was developed as an experimental platform for the practice of dependently typed programming and extends the 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 the Agda language into untyped λ-calculus encoded in Haskell. The second feature is the application of the Haskell class mechanism to embed typed Haskell terms in the universal type for untyped λ-calculus. This approach makes Agate very lightweight. The performance of a number of codes generated by Agate is evaluated.

Journal

• Computer Software

  Computer Software 26 (4), 107-119, 2009

  Japan Society for Software Science and Technology

Details

• CRID: 1390282679713060736
• NII Article ID: 130004549149
• DOI: 10.11309/jssst.26.4_107
• ISSN: 02896540
• Data Source:
  • JaLC
  • CiNii Articles
  • KAKEN
• Abstract License Flag: Disallowed