延迟单值函数中的求值归一化安德烈亚斯·阿贝尔和詹姆斯·查普曼(MSFP 2014).
类型理论中类型理论转换的判定安德烈亚斯·阿贝尔(Andreas Abel),约阿金·赫曼(Joakimhman)和安德烈亚·维佐西(Andrea Vezzosi)(2018年流行音乐节).
保护递归类型强正规化的形式化证明Andreas Abel和Andrea Vezzosi(APLAS 2014).
大小依赖类型的求值归一化Andreas Abel,Andrea Vezzosi和Theo Winterhalter(2017年ICFP).
通过依赖类型语法进行类型保护编译安德烈亚斯·阿贝尔(类型2020)
Agda中的正则表达式作者:Alexandre Agular和Bassel Mannaa(技术报告,2009年)
通过评估和代数效应归一化Danel Ahman和Sam Staton(MFPS 2013).
同伦类型理论中的非wellfounded树Benedikt Ahrens,Paolo Capriotti和Régis Spadotti(TLCA 2015)
有序范畴中的机械化关系代数序理论Musa Al-hassy和Wolfram Kahl,RAMICS 2014.
带有多余部分的打字 -  - 直觉主义线性逻辑的机械化纪尧姆·阿拉斯(2017年诉讼后类型).
类型和范围安全程序及其证明纪尧姆·阿拉斯,詹姆斯·查普曼,康诺·麦克布莱德,詹姆斯·麦金纳(CPP 2017)
泛型级多晶N元函数作者:Allais Guillaume(TYDE 2019)
单子不一定是内函子托尔斯滕·阿滕科奇,詹姆斯·查普曼和塔尔莫·乌斯塔鲁(FoSSaCS 2010).
单子不一定是内函子托尔斯滕·阿滕科奇,詹姆斯·查普曼和塔尔莫·乌斯塔鲁(LMCS 2015).
相对单子形式化托尔斯滕·阿滕科奇,詹姆斯·查普曼和塔尔莫·乌斯塔鲁(JFR 2014).
嵌套电感和共导型的终端检查托尔斯滕·阿滕科奇和尼尔斯·安德斯·丹尼尔森.
使用商归纳类型的类型理论中的类型理论托尔斯滕·阿滕科奇和安布罗斯·卡波西(POPL 2016).
依赖类型评估归一化Thorsten Altenkirch和Ambrus Kaposi(FSCD 2016).
ω-群胚的一些构造Thorsten Altenkirch,Nuo Li和Ondr ej Rypáček(LFMTP 2014).
弱ω-群胚的句法研究Thorsten Altenkirch和Ondřej Rypáckek(CSL 2012;随附Agda形式化).
从终止证明中提取Call-by-Name部分求值器作者:Kenichi Asai(PEPM 2019,正式化)
部分求值的一种类型理论说明作者:Kenichi Asai,Luminus Fennell,Peter Thiemann和Yang Zhang(PPDP 2014)
认证的上下文无关解析:在Agda中对Valiant算法进行形式化.Jean-Philippe Bernardy和Patrik Jansson,2016年.
在Logipedia中导入Agda Proofs作者:弗雷德里克·布兰基(Frédéric Blanqui)和纪尧姆·Genestier(MSc实习,2019年)
工作中的依赖类型Ana Bove和Peter Dybjer(LerNet ALFA夏令营2008).
函数程序一阶理论中交互推理与自动推理的结合作者:Ana Bove,Peter Dybjer和Andrés Sicard-Ramírez(FoSSaCS 2012).
在Agda中嵌入结构逻辑理论作者:Ana Bove,Peter Dybjer和Andrés Sicard-Ramírez(PLPV 2009).
高阶语言的变化理论通过静态微分递增λ-演算蔡玉飞,保罗·贾鲁索,蒂尔曼·伦德尔和克劳斯·奥斯特曼(PLDI 2014;正式化的)
Agda中构造射影几何的形式化吉列尔莫·卡尔德龙(LSFA 2017;Agda形式化)
结构动态非因果建模语言的形式语义John Capper和Henrik Nilsson(TLDI 2012).
半环与弱Rig群胚的计算Jacques Carette和Amr Sabry(2016年员工持股计划).
将数学知识形式化为双形式理论图:一个案例研究作者:Jacques Carette,William M.Farmer
利用弱双相似性对时滞单子进行商作者:James Chapman,Tarmo Uustalu,NiccolóVeltri(ICTAC 2015).
利用弱双相似性对时滞单子进行商James Chapman,Tarmo Uustalu,NiccolóVeltri(MSCS 2019).
分数类型:Ancilla比特的表达式和安全空间管理作者:Chao-Hong Chen,Vikraman Choudhury,Jacques Carette,Amr Sabry
基于反射的一元型策略规划作者:Liang-Ting Chen(TYDE 2019)
贪婪算法从关系规范的形式化推导:教程由Yu-Hsi Chiang和Shin-Cheng Mu(JLAMP,新闻稿)撰写.
Agda中的灵活硬币制作作者:Luca Ciccone(硕士论文)
重叠和顺序依赖模式:所有人的定义相等Jesper Cockx,Dominique Devriese和Frank Piessens(ESOP 2014).
为您的香草型理论提供一些扩展性Jesper Cockx和Andreas Abel(TYPES 2016),扩展摘要.
作为等价物的统一:相关类型数据的相关验证统一Jesper Cockx,Dominique Devriese和Frank Piessens(ICFP 2016).
会话类型的主体类型方案作者:Ernesto Copello,Nora Szasz和Alvaro Tasistro(国际逻辑与计算杂志;随附Agda代码).
(相当)无痛依赖类型编程案例:Agda中完全认证的合并排序埃内斯托·科佩罗,阿尔瓦罗·塔西斯特罗和布鲁诺·比安奇(SBLP 2014).
巴伦德雷格特(Barendregt)关于带粘结剂的一般结构的可变约定的构造类型理论形式化作者:Ernesto Copello,Nora Szasz,Alvaro Tasistro(FSCD的LFMTP 2018: 11-26).
计算最密集段问题的线性时间解Sharon Curtis和Shin-Cheng Mu(2015年JFP;Agda形式化).
跨饰品传输功能Pierre-Evariste Dagand和Conor McBride(2012年国际电影节;Agda模型).
跨饰品传输功能皮埃尔·埃瓦里斯特·达甘和康诺·麦克布莱德(JFP;Agda模型).
脲醛树脂的弛豫和Agda中的Dubois异步定点理论作者:Matthew Daggit,Ran Zmigrod和Timothy G.Griffin(2019年1月)
依赖类型语言作为归纳-递归族的形式化作者:Nils Anders Danielsson(类型2006).(用途AgdaLight公司阿格达的近亲.)
"纯功能数据结构的轻量级半形式时间复杂性分析"正确性结果的形式化尼尔斯·安德斯·丹尼尔森.
基于证明相关隶属关系的袋等价作者:Nils Anders Danielsson(ITP 2012).
使用嵌入式语言击败生产力检查器作者:Nils Anders Danielsson(PAR 2010).
纯函数数据结构的轻量级半形式时间复杂度分析尼尔斯·安德斯·丹尼尔森(POPL 2008).
使用偏单数的操作语义Nils Anders Danielsson(2012年ICFP).
声明性地分型:混合归纳法和共归纳法练习Nils Anders Danielsson和Thorsten Altenkirch(MPC 2010).
机械验证计算抽象解释作者:David Darais和David Van Horn.
类型化语法元编程Dominique Devriese和Frank Piessens(ICFP 2013).
通过依赖类型验证基于堆栈的遗传编程Larry Diehl(AAIP 2011).
升级依赖类型:通用谓词层次结构上的泛型编程.作者:Larry Diehl和Tim Sheard(DTP 2013).
描述中的泛型构造函数和消除器:作为依赖类型内部DSL的类型理论作者:Larry Diehl和Tim Sheard(WGP 2014).
无限感应递归类型的通用查找和更新作者:Larry Diehl和Tim Sheard
二元简单类型理论哈利·伊德斯三世,亚伦·斯塔姆和瑞恩·麦克莱里(LMCS 2016)
提出一种新的单体范畴攻击树基础哈雷·伊德斯III
在任何种类的构造数学中满足全知原则的无限集作者:Martin Escardó(JSL 2013,第78卷(3)).
通过有效强迫实现哥德尔系统T泛函的连续性Martin Escardó,MFPS'2013.ENTCS 01/2013;298:119-141.
Martin-Löf宇宙的内在拓扑Martin Escardó,4WFT(形式拓扑第四次研讨会),斯洛文尼亚卢布尔雅那,2012年6月(Agda代码).
可搜索集合,Dubuc-Penon紧性,全能科学原理和酒鬼悖论作者:马特·恩·埃斯卡多和保罗·奥利瓦(CiE 2010小册子;Agda代码).
序列博弈,Tychonoff定理和双负移位有什么共同点马丁·埃斯卡多和保罗·奥利瓦(MSFP 2010).
Martin-Lo¨f宇宙的本征拓扑作者:马特·恩·霍泽尔·埃斯卡多和托马斯·斯特里彻(发表于"纯粹和应用逻辑年鉴";参考Agda代码).
Kleene-Kreisel连续泛函的构造性表现作者:Martín Escardoí和Chuangjie Xu(被"纯粹逻辑与应用逻辑年鉴"接受出版;Agda代码).
Brouwerian连续性原则与Curry-Howard解释的不一致性作者:Martin Escardó和Chuangjie Xu,TLCA'2015.
常规语言的认证分析Denis Firsov和Tarmo Uustalu(CPP 2013).
无上下文语言的CYK认证解析Denis Firsov和Tarmo Uustalu(JLAMP 2014).
上下文无关文法的认证规范化Denis Firsov和Tarmo Uustalu(CPP 2015).
有限集依赖型规划Denis Firsov和Tarmo Uustalu(WGP 2015).
Noetherianess的变体Denis Firsov,Tarmo Uustalu和NiccolóVeltri(MSFP 2016).
埃斯特雷尔的微积分:如果可以,可以.如果不行,就不行由Spencer P.Florence,Shu-Hung You,Jesse A.Tov和Robby Findler创作(2019年流行音乐节).
将自动定理证明程序集成到Agda中Simon Foster和Georg Struth(第三届NASA正式方法研讨会).
归纳递归和索引归纳递归的代数基础与实现尼尔·加尼(Neil Ghani)和彼得·汉考克(Peter Hancock).
无K的定义证明相关Gaetan Gilbert,Jesper Cockx,Matthieu Sozeau和Nicolas Tabarau(2019年流行音乐节).
循环共享树结构的初始代数语义作者Makoto Hamana(LMCS 2010).
GADT和归纳族的基础:相关多项式Functor方法Makoto Hamana和Marcelo Fiore(WGP 2011).
同伦理论机械化中的高维类型作者:Kuen-Bang Hou(Favonia),博士论文.
科学计算中的依赖型编程:经济建模示例通过塞扎尔·伊奥内斯库和帕特里克·詹森(IFL 2012).
气候影响研究中的测试与证明通过塞扎尔·伊奥内斯库和帕特里克·詹森(类型2011).
如何证明:实际证明有效程序结果的属性(函数珍珠)由Koen Jacobs,Andreas Nuyts,Dominique Devriese编写(TYDE 2019)
流I/O的松弛编织结构作者:Alan Jeffrey和Julian Rathke(CSL 2011).
链接数据的完整性约束由Alan Jeffrey和Peter F.Patel Schneider编写(DL 2011).
因果关系免费!:参数性意味着功能反应性程序的因果关系Alan Jeffrey(PLPV 2013).
依赖类型的Web客户端应用程序:HTML5中Agda中的FRPAlan Jeffrey(PADL 2013).
类型化项图的相关类型形式化沃尔夫拉姆·卡尔,TERMGRAPH 2011.
关系代数抽象的依赖型形式化Wolfram Kahl,RAMICS 2011.
基于关系范畴的图变换的可证明实现Wolfram Kahl,RAMICS 2012.
概念格的机械化抽象形式化Wolfram Kahl,RAMICS 2014.
自动定理证明与交互式定理证明的轻量级集成卡里姆·卡索(Karim Kanso)和安东·塞泽尔(Anton Setzer).
简单类型的遗传替代,形式化Chantal Keller和Thorsten Altenkirch(MSFP 2010).
Setoid的范畴理论结构Yoshiki Kinoshita和John Power(TCS).
Agda中类型逻辑语法的形式化Pepijn Kokke(泰勒斯).
Agda中的自动:使用反射进行编程验证搜索Pepijn Kokke和Wouter Swierstra(MPC 2015).
正则表达式匹配器的内部验证作者:Joomy Korkut,Maksim Trifunovski和Daniel R.Licata.
Hedberg定理的推广由Nicolai Kraus,Martín Escardó,Thierry Coquand和Thorsten Altenkirch编写(TLCA 2013;在Agda中正式化).
单价宇宙层次中的高级同伦Nicolai Kraus和Christian Sattler(美国计算机学会计算逻辑汇刊;Agda形式化).
马丁·洛夫类型理论中的匿名存在概念由Nicolai Kraus,M.H.Escardo,T.Coquand和T.Altenkirch提交给LMCS.
同伦类型理论中的截断水平尼古拉·克劳斯博士论文.
非安全高电感类型的结构作者:Nicolai Kraus,LICS 2016.
Agda作为开发经验证的铁路联锁系统的平台.Karim Kanso博士论文.
合成同伦理论的立方方法Daniel R.Licata和Guillaume Brunerie(LICS 2015).
同伦型理论中的πn(Sn)作者Daniel R.Licata和Guillaume Brunerie(特邀论文,CPP 2013;使用Agda正式证明).
同伦型理论中的Eilenberg-MacLane空间Dan Licata和Eric Finster(LICS 2014;随附Agda正式化).
绑定和计算的世界作者Daniel R.Licata和Robert Harper(ICFP 2009).
具有2类模式的伴随逻辑作者Daniel R.Licata和Michael Shulman(LFCS 2016;参考Agda证明).
同伦型理论中圆的基本群的计算作者Daniel R.Licata和Michael Shulman(LICS 2013).
带索引函数的泛型编程Andres Löh和JoséPedro Magalháes(WGP 2011).
广义道的认证Foata归一化Hendrik Maarand和Tarmo Uustalu(NFM 2018).
广义迹的认证归一化亨德里克·马兰德和塔尔莫·乌斯塔卢(ISSE 2019).
多项式检验原理由Conor McBride创作.
装饰代数,代数装饰由Conor McBride创作.
令人发指但有意义的巧合:依赖类型安全语法和评估Conor McBride(WGP 2010).
用依赖类型语言编写代数程序的经验Sergei D.Meshveliani(PCA,2014年).
关于程序设计数学中的依赖类型和直觉主义由С.Д. 梅什韦利亚尼(S.D.Meshveliani).
关于列表处理的可证明程序Sergei D.Meshveliani(PCA'2015).
ПрОГраммированиеоснааиитеатнотаоаЛебррттиннтонкауикесависмриТиПаМи(用相关类型的语言由С.Д. 梅斯韦利亚尼.
内省Kripke模型和λ评估归一化-微积分作者:Miötek Bak
依赖型编程中的安全型编程Jamie Morgenstern和Daniel R.Licata(ICFP 2010).
Agda中的编程代数:关系程序派生的依赖类型作者:Shin-Cheng Mu,Xiang-Shang Ko和Patrik Jansson(JFP 2009).
异步电路的定理证明验证作者:西村顺治,Amagasaki,Kuga,Iida Masahiro,Sueyoshi Toshinori(国际创新计算,信息和控制杂志).
立方Agda中的三个等价序数符号系统作者:Fredrik Nordvall Forsberg,Chuangjie Xu,Neil Ghani(CPP 2020)
Agda中的依赖类型编程作者:乌尔夫·诺雷尔(AFP 2008).
依赖类型的交互式编程Ulf Norell(受邀演讲,ICFP 2013;来自谈话的Agda代码).
应用证明搜索的应用利亚姆·奥康纳(TYDE 2016)
带类型孔的实时函数编程Cyrus Omar,Ian Voysey,Ravi Chugh和Matthew A.Hammer,POPL 2019.
使用会话类型作为效果系统Dominic Orchard和Nobuko Yoshida(2015年地点;Agda形式化).
Topos中立方型理论的建模公理作者:I.Orton和A.M.Pitts,CSL 2016.
用活页夹统一处理语法尼古拉斯·鲍伊拉德和弗朗索瓦·波蒂埃(JFP 2012)
Agda中的模块化安全防护Christopher Schwaab和Jeremy G.Siek(PLPV 2013).
通过依赖类型的安全功能反应式编程Neil Sculthorpe和Henrik Nilsson(ICFP 2009).
构造可证明逻辑由Robert J.Simmons和Bernardo Toninho撰写(2011年IMLA上发表).
从数学到抽象机器:可执行Krivine机器的形式化推导作者:Wouter Swierstra(MSFP 2012).
分布式阵列的更多依赖类型作者:Wouter Swierstra(HOSC 2010).
分类:验证荷兰国旗的类型理论问题作者:Wouter Swierstra(JFP 2011).
分布式阵列的依赖类型作者:Wouter Swierstra和Thorsten Altenkirch(TFP 2008).
多态动态类型库作者:Wouter Swierstra和Thomas van Noort.
Stoughton替代Lambda演算的构造型理论形式化作者:阿尔瓦罗·塔西斯特罗,埃内斯托·科佩罗和诺拉·萨兹(LSFA 2014).
从代数到抽象机:一个经过验证的泛型结构Carlos ToméCortiñas和Wouter Swierstra(TyDe 2018).
有限性和有理数列,建设性地由Tarmo Uustalu和NiccolóVeltri撰写(JFP 2017).
偏爱和容器单子由Tarmo Uustalu和NiccolóVeltri编写(2017年APLAS).
延迟单子和限制类别由Tarmo Uustalu和NiccolóVeltri编写(ICTAC 2017).
斜单体范畴的序列演算作者:塔尔莫·乌斯塔卢,尼科洛·维尔特里和诺姆·泽尔伯格(MFPS XXXIV).
部分正规斜单体范畴的证明理论塔尔莫·乌斯塔卢,尼科洛·维尔特里和诺姆·泽尔伯格(ACT 2020)
Agda中反射的工程证明Paul van der Walt和Wouter Swierstra(IFL 2012).
论信息流控制库的形式化马可·瓦塞纳(Marco Vassena)和亚历杭德罗·拉索(Alejandro Russo)(2016年公共安全局).
类型理论中基于集合的商的两种实现作者:NiccolóVeltri(SPLST 2015).
Agda中通过大小类型的保护递归NiccolóVeltri和Niels van der Weide(FSCD 2019).
模式统一的范畴观安德烈亚·维佐西和安德烈亚斯·阿贝尔(UNIF 2014).
立方Agda:一种具有单价和更高归纳类型的依赖类型编程语言Andrea Vezzosi,Anders Mörtberg和Andreas Abel(2019年ICFP).
Arit-通用数据类型-通用编程斯蒂芬妮·魏里奇和克里斯·卡辛基诺(PLPV 2010).
一致连续的构造模型作者:Chuangjie Xu和M.H.Escardo,TLCA 2013.
聚焦和高阶抽象语法作者Noam Zeilberger(POPL 2008;论文没有提到Agda,但一些附带的Agda代码是可获得的).