A Brief Overview of Agda - A Functional Language with Dependent Types

被引：0
|
作者：
Bove, Ana [1 ]
Dybjer, Peter [1 ]
Norell, Ulf [1 ]
机构：
[1] Chalmers Univ Technol, S-41296 Gothenburg, Sweden
来源：
THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS | 2009年 / 5674卷
关键词：
D O I：
暂无
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
We give an overview of Agda, the latest in a series of dependently typed programming languages developed in Gothenburg. Agda is based oil Martin-Lof's intuitionistic type theory but extends it with numerous programming language features. It supports a wide range of inductive data types, including inductive families and inductive-recursive types, with associated flexible pattern-snatching. Unlike other proof assistants, Agda is not, tactic-based. Instead it has all Emacs-based interface which allows programming by gradual refinement of incomplete type-correct terms.
引用
收藏
页码：73 / 78
页数：6
相关论文
共 50 条
  • [1] Agda-curious? An Exploration of Programming with Dependent Types
    McBride, Conor
    ACM SIGPLAN NOTICES, 2012, 47 (09) : 1 - 2
  • [2] Algebra of programming in Agda: Dependent types for relational program derivation
    Mu, Shin-Cheng
    Ko, Hsiang-Shang
    Jansson, Patrik
    JOURNAL OF FUNCTIONAL PROGRAMMING, 2009, 19 : 545 - 579
  • [3] A brief overview of crusher types
    不详
    ZKG INTERNATIONAL, 2006, 59 (04): : 22 - +
  • [4] Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types
    Vezzosi, Andrea
    Mortberg, Anders
    Abel, Andreas
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2019, 3 (ICFP):
  • [5] Cubical Agda: A dependently typed programming language with univalence and higher inductive types
    Vezzosi, Andrea
    Mortberg, Anders
    Abel, Andreas
    JOURNAL OF FUNCTIONAL PROGRAMMING, 2021, 31
  • [6] Programming language foundations in Agda
    Kokke, Wen
    Siek, Jeremy G.
    Wadler, Philip
    SCIENCE OF COMPUTER PROGRAMMING, 2020, 194
  • [7] Verified Functional Programming in Agda
    Pradella, Matteo
    FORMAL ASPECTS OF COMPUTING, 2024, 36 (01)
  • [8] Sytemic Functional Linguistics: a brief overview
    dos Santos, Zaira Bomfante
    SOLETRAS, 2014, (28): : 164 - 181
  • [9] Foreign language education in the PRC - A brief overview
    Mao, LM
    Min, Y
    LANGUAGE POLICY IN THE PEOPLE'S REPUBLIC OF CHINA: THEORY AND PRACTICE SINCE 1949, 2004, 4 : 319 - 329
  • [10] Cayenne - a language with dependent types
    Augustsson, L
    ACM SIGPLAN NOTICES, 1999, 34 (01) : 239 - 250
12345