Dependently Typed Programming in Agda

被引:0
|
作者
Norell, Ulf [1 ]
机构
[1] Chalmers, S-41296 Gothenburg, Sweden
来源
ADVANCED FUNCTIONAL PROGRAMMING | 2009年 / 5832卷
关键词
D O I
暂无
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
引用
收藏
页码:230 / 266
页数:37
相关论文
共 50 条
  • [1] 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):
  • [2] 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
  • [3] Case of (Quite) Painless Dependently Typed Programming: Fully Certified Merge Sort in Agda
    Copello, Ernesto
    Tasistro, Alvaro
    Bianchi, Bruno
    PROGRAMMING LANGUAGES, SBLP 2014, 2014, 8771 : 62 - 76
  • [4] Dependently typed programming
    Mu, Shin-Cheng
    Mcbride, Conor
    Weirich, Stephanie
    Progress in Informatics, 2013, (10): : 149 - 155
  • [5] Dependently Typed Programming with Singletons
    Eisenberg, Richard A.
    Weirich, Stephanie
    ACM SIGPLAN NOTICES, 2012, 47 (12) : 117 - 129
  • [6] Dependently Typed Programming Preface
    Altenkirch, Thorsten
    Uustalu, Tarmo
    FUNDAMENTA INFORMATICAE, 2010, 102 (02) : I - I
  • [7] Security-Typed Programming within Dependently Typed Programming
    Morgenstern, Jamie
    Licata, Daniel R.
    ICFP 2010: PROCEEDINGS OF THE 2010 ACM SIGPLAN INTERNATIONAL CONFERENCE ON FUNCTIONAL PROGRAMMING, 2010, : 169 - 180
  • [8] Security-Typed Programming within Dependently Typed Programming
    Morgenstern, Jamie
    Licata, Daniel R.
    ACM SIGPLAN NOTICES, 2010, 45 (09) : 169 - 180
  • [9] Generic programming within dependently typed programming
    Altenkirch, T
    McBride, C
    GENERIC PROGRAMMING, 2003, 115 : 1 - 20
  • [10] Automation for Dependently Typed Functional Programming
    Wilson, Sean
    Fleuriot, Jacques
    Smaill, Alan
    FUNDAMENTA INFORMATICAE, 2010, 102 (02) : 209 - 228