Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
101 | Ulf Norell |
Dependently typed programming in Agda. |
TLDI |
2009 |
DBLP DOI BibTeX RDF |
programming, dependent types |
82 | Ana Bove, Peter Dybjer, Ulf Norell |
A Brief Overview of Agda - A Functional Language with Dependent Types. |
TPHOLs |
2009 |
DBLP DOI BibTeX RDF |
|
82 | Ana Bove, Peter Dybjer, Andrés Sicard-Ramírez |
Embedding a logical theory of constructions in Agda. |
PLPV |
2009 |
DBLP DOI BibTeX RDF |
general recursion, logical theory of constructions, type theory |
82 | Fredrik Lindblad, Marcin Benke |
A Tool for Automated Theorem Proving in Agda. |
TYPES |
2004 |
DBLP DOI BibTeX RDF |
|
78 | Andreas Abel 0001, Marcin Benke, Ana Bove, John Hughes 0001, Ulf Norell |
Verifying haskell programs using constructive type theory. |
Haskell |
2005 |
DBLP DOI BibTeX RDF |
GHC core, monadic translation, verification, haskell, type theory, partiality |
58 | Ana Bove, Peter Dybjer |
Dependent Types at Work. |
LerNet ALFA Summer School |
2008 |
DBLP DOI BibTeX RDF |
|
52 | Stephanie Weirich, Chris Casinghino |
Arity-generic datatype-generic programming. |
PLPV |
2010 |
DBLP DOI BibTeX RDF |
agda, arity-generic programming, generic haskell, dependent types |
52 | Daniel R. Licata, Robert Harper 0001 |
Positively dependent types. |
PLPV |
2009 |
DBLP DOI BibTeX RDF |
agda, dependent types, polarity |
41 | Zahra Gharaee, ZeMing Gong, Nicholas Pellegrino, Iuliia Zarubiieva, Joakim Bruslund Haurum, Scott C. Lowe, Jaclyn T. A. McKeown, Chris C. Y. Ho, Joschka McLeod, Yi-Yun C. Wei, Jireh Agda, Sujeevan Ratnasingham, Dirk Steinke, Angel X. Chang, Graham W. Taylor, Paul W. Fieguth |
A Step Towards Worldwide Biodiversity Assessment: The BIOSCAN-1M Insect Dataset. |
CoRR |
2023 |
DBLP DOI BibTeX RDF |
|
41 | Zahra Gharaee, ZeMing Gong, Nicholas Pellegrino, Iuliia Zarubiieva, Joakim Bruslund Haurum, Scott C. Lowe, Jaclyn T. A. McKeown, Chris C. Y. Ho, Joschka McLeod, Yi-Yun C. Wei, Jireh Agda, Sujeevan Ratnasingham, Dirk Steinke, Angel X. Chang, Graham W. Taylor, Paul W. Fieguth |
A Step Towards Worldwide Biodiversity Assessment: The BIOSCAN-1M Insect Dataset. |
NeurIPS |
2023 |
DBLP BibTeX RDF |
|
41 | Agda L. G. Oliveira, Joaquim P. Lima, Thiago L. Brasco, Lucas R. Amaral |
The importance of modeling the effects of trend and anisotropy on soil fertility maps. |
Comput. Electron. Agric. |
2022 |
DBLP DOI BibTeX RDF |
|
41 | Veridianna Cristina Teodoro Ferreira, Agda Carvalho |
Thermoregulating and Hydrating Microcapsules: Contributions of Textile Technology in the Design of Wearable Products for Wheelchair Dependents. |
HCI (17) |
2019 |
DBLP DOI BibTeX RDF |
|
41 | Veridianna Cristina Teodoro Ferreira, Agda Carvalho |
Inclusive Design and Textile Technology in the Everyday Lives of Wheelchair Dependent. |
HCI (17) |
2018 |
DBLP DOI BibTeX RDF |
|
41 | Priscila Trovo, Adriana Valli, Nivia Ferreira, Agda Carvalho |
Interaction/Cognition in Design: The Red Bull Station's Classroom Case Study. |
HCI (21) |
2017 |
DBLP DOI BibTeX RDF |
|
41 | Wanding Zhou, Tenghui Chen, Hao Zhao, Agda Karina Eterovic, Funda Meric-Bernstam, Gordon B. Mills, Ken Chen 0001 |
Bias from removing read duplication in ultra-deep sequencing experiments. |
Bioinform. |
2014 |
DBLP DOI BibTeX RDF |
|
39 | Noam Zeilberger |
Refinement types and computational duality. |
PLPV |
2009 |
DBLP DOI BibTeX RDF |
duality, effects, intersection types, focusing, union types |
39 | Neil Sculthorpe, Henrik Nilsson |
Safe functional reactive programming through dependent types. |
ICFP |
2009 |
DBLP DOI BibTeX RDF |
DSELS, FRP, synchronous data-flow, functional programming, domain-specific languages, dependent types, reactive programming |
39 | Yoshifumi Yuasa, Yoshinori Tanabe, Toshifusa Sekizawa, Koichi Takahashi |
Verification of the Deutsch-Schorr-Waite Marking Algorithm with Modal Logic. |
VSTTE |
2008 |
DBLP DOI BibTeX RDF |
|
39 | Peter Dybjer, Qiao Haiyan, Makoto Takeyama |
Combining Testing and Proving in Dependent Type Theory. |
TPHOLs |
2003 |
DBLP DOI BibTeX RDF |
|
24 | Donnacha Oisín Kidney, Zhixuan Yang, Nicolas Wu |
Algebraic Effects Meet Hoare Logic in Cubical Agda. |
Proc. ACM Program. Lang. |
2024 |
DBLP DOI BibTeX RDF |
|
24 | Antoine Van Muylder, Andreas Nuyts, Dominique Devriese |
Internal and Observational Parametricity for Cubical Agda. |
Proc. ACM Program. Lang. |
2024 |
DBLP DOI BibTeX RDF |
|
24 | Maximilian Doré, Evan Cavallo, Anders Mörtberg |
Automating Boundary Filling in Cubical Agda. |
CoRR |
2024 |
DBLP DOI BibTeX RDF |
|
24 | Matteo Pradella |
Review on Verified Functional Programming in Agda: By Aaron Stump ACM, ISBN: 978-1-97000-126-6, 246 pages, 2016. |
Formal Aspects Comput. |
2024 |
DBLP DOI BibTeX RDF |
|
24 | Cosmo Viola, Max Fan, Talia Ringer |
Towards Proof Repair in Cubical Agda. |
CoRR |
2023 |
DBLP DOI BibTeX RDF |
|
24 | Axel Ljungström, Anders Mörtberg |
Formalizing π4(S^3) ≅ ℤ/2ℤ and Computing a Brunerie Number in Cubical Agda. |
CoRR |
2023 |
DBLP DOI BibTeX RDF |
|
24 | Niccolò Veltri, Andrea Vezzosi |
Formalizing CCS and π-calculus in Guarded Cubical Agda. |
J. Log. Algebraic Methods Program. |
2023 |
DBLP DOI BibTeX RDF |
|
24 | Axel Ljungström, Anders Mörtberg |
Formalizing π4(S3) ≅Z/2Z and Computing a Brunerie Number in Cubical Agda. |
LICS |
2023 |
DBLP DOI BibTeX RDF |
|
24 | Fahad F. Alhabardi, Anton Setzer |
A model of Solidity-style smart contracts in the theorem prover Agda. |
AIBThings |
2023 |
DBLP DOI BibTeX RDF |
|
24 | Thomas Lamiaux, Axel Ljungström, Anders Mörtberg |
Computing Cohomology Rings in Cubical Agda. |
CPP |
2023 |
DBLP DOI BibTeX RDF |
|
24 | Joris Ceulemans, Andreas Nuyts, Dominique Devriese |
Sikkel: Multimode Simple Type Theory as an Agda Library. |
MSFP@ETAPS |
2022 |
DBLP DOI BibTeX RDF |
|
24 | Harold Carr, Christopher Jenkins, Mark Moir, Victor Cacciari Miraldo, Lisandra Silva |
Towards Formal Verification of HotStuff-based Byzantine Fault Tolerant Consensus in Agda: Extended Version. |
CoRR |
2022 |
DBLP DOI BibTeX RDF |
|
24 | Fahad F. Alhabardi, Arnold Beckmann, Bogdan Lazar, Anton Setzer |
Verification of Bitcoin's Smart Contracts in Agda using Weakest Preconditions for Access Control. |
CoRR |
2022 |
DBLP DOI BibTeX RDF |
|
24 | Sebastián Urciuoli |
A Formal Proof of the Strong Normalization Theorem for System T in Agda. |
LSFA |
2022 |
DBLP DOI BibTeX RDF |
|
24 | Thomas Lamiaux, Axel Ljungström, Anders Mörtberg |
Computing Cohomology Rings in Cubical Agda. |
CoRR |
2022 |
DBLP DOI BibTeX RDF |
|
24 | Zachary Murray |
Constructive Analysis in the Agda Proof Assistant. |
CoRR |
2022 |
DBLP DOI BibTeX RDF |
|
24 | Miguel Pagano, José E. Solsona |
Nominal Sets in Agda - A Fresh and Immature Mechanization. |
LSFA |
2022 |
DBLP DOI BibTeX RDF |
|
24 | Harold Carr, Christa Jenkins, Mark Moir, Victor Cacciari Miraldo, Lisandra Silva |
An approach to translating Haskell programs to Agda and reasoning about them. |
CoRR |
2022 |
DBLP DOI BibTeX RDF |
|
24 | Stephen Dolan |
Computing with generic trees in Agda. |
TyDe@ICFP |
2022 |
DBLP DOI BibTeX RDF |
|
24 | Harold Carr, Christa Jenkins, Mark Moir, Victor Cacciari Miraldo, Lisandra Silva |
Towards Formal Verification of HotStuff-Based Byzantine Fault Tolerant Consensus in Agda. |
NFM |
2022 |
DBLP DOI BibTeX RDF |
|
24 | Guillaume Brunerie, Axel Ljungström, Anders Mörtberg |
Synthetic Integral Cohomology in Cubical Agda. |
CSL |
2022 |
DBLP DOI BibTeX RDF |
|
24 | Jesper Cockx, Orestis Melkonian, Lucas Escot, James Chapman 0001, Ulf Norell |
Reasonable Agda is correct Haskell: writing verified Haskell using agda2hs. |
Haskell |
2022 |
DBLP DOI BibTeX RDF |
|
24 | Samuel da Silva Feitosa, Rodrigo Geraldo Ribeiro, André Rauber Du Bois |
Towards an Extrinsic Formalization of Featherweight Java in Agda. |
CLEI Electron. J. |
2021 |
DBLP DOI BibTeX RDF |
|
24 | William J. DeMeo |
The Agda Universal Algebra Library, Part 1: Foundation. |
CoRR |
2021 |
DBLP BibTeX RDF |
|
24 | William J. DeMeo |
The Agda Universal Algebra Library, Part 2: Structure. |
CoRR |
2021 |
DBLP BibTeX RDF |
|
24 | Gan Shen, Lindsey Kuper |
Toward SMT-Based Refinement Types in Agda. |
CoRR |
2021 |
DBLP BibTeX RDF |
|
24 | Andreas Abel 0001 |
Birkhoff's Completeness Theorem for Multi-Sorted Algebras Formalized in Agda. |
CoRR |
2021 |
DBLP BibTeX RDF |
|
24 | William J. DeMeo |
The Agda Universal Algebra Library and Birkhoff's Theorem in Martin-Löf Dependent Type Theory. |
CoRR |
2021 |
DBLP BibTeX RDF |
|
24 | Victor Cacciari Miraldo, Harold Carr, Mark Moir, Lisandra Silva, Guy L. Steele Jr. |
Formal Verification of Authenticated, Append-Only Skip Lists in Agda: Extended Version. |
CoRR |
2021 |
DBLP BibTeX RDF |
|
24 | Louis Warren |
First-order natural deduction in Agda. |
CoRR |
2021 |
DBLP BibTeX RDF |
|
24 | Andrea Vezzosi, Anders Mörtberg, Andreas Abel 0001 |
Cubical Agda: A dependently typed programming language with univalence and higher inductive types. |
J. Funct. Program. |
2021 |
DBLP DOI BibTeX RDF |
|
24 | Fahad F. Alhabardi, Arnold Beckmann, Bogdan Lazar, Anton Setzer |
Verification of Bitcoin Script in Agda Using Weakest Preconditions for Access Control. |
TYPES |
2021 |
DBLP DOI BibTeX RDF |
|
24 | Guillermo Calderón |
Formalizing Affinization of a Projective Plane in Agda. |
CLEI |
2021 |
DBLP DOI BibTeX RDF |
|
24 | Luca Ciccone, Francesco Dagnino, Elena Zucca |
Flexible Coinduction in Agda. |
ITP |
2021 |
DBLP DOI BibTeX RDF |
|
24 | Victor Cacciari Miraldo, Harold Carr, Mark Moir, Lisandra Silva, Guy L. Steele Jr. |
Formal verification of authenticated, append-only skip lists in Agda. |
CPP |
2021 |
DBLP DOI BibTeX RDF |
|
24 | Jason Z. S. Hu, Jacques Carette |
Formalizing category theory in Agda. |
CPP |
2021 |
DBLP DOI BibTeX RDF |
|
24 | Uma Zalakain, Ornela Dardha |
π with Leftovers: A Mechanisation in Agda. |
FORTE |
2021 |
DBLP DOI BibTeX RDF |
|
24 | Jason Z. S. Hu, Jacques Carette |
Proof-relevant Category Theory in Agda. |
CoRR |
2020 |
DBLP BibTeX RDF |
|
24 | Uma Zalakain, Ornela Dardha |
π with leftovers: a mechanisation in Agda. |
CoRR |
2020 |
DBLP BibTeX RDF |
|
24 | Pierre Lescanne |
Extensive Infinite Games and Escalation, an exercise in Agda. |
CoRR |
2020 |
DBLP BibTeX RDF |
|
24 | Luca Ciccone |
Flexible Coinduction in Agda. |
CoRR |
2020 |
DBLP BibTeX RDF |
|
24 | Matthew L. Daggitt, Ran Zmigrod, Timothy G. Griffin |
A Relaxation of Üresin and Dubois' Asynchronous Fixed-Point Theory in Agda. |
J. Autom. Reason. |
2020 |
DBLP DOI BibTeX RDF |
|
24 | Wen Kokke, Jeremy G. Siek, Philip Wadler |
Programming language foundations in Agda. |
Sci. Comput. Program. |
2020 |
DBLP DOI BibTeX RDF |
|
24 | Santiago Arranz Olmos, Martín Fernández, Matías Steinberg, Alejandro Gadea, Emmanuel Gunther, Miguel Pagano |
A formalisation of LEGv8 in Agda. |
SBLP |
2020 |
DBLP DOI BibTeX RDF |
|
24 | Guillaume Genestier |
Encoding Agda Programs Using Rewriting. |
FSCD |
2020 |
DBLP DOI BibTeX RDF |
|
24 | Cecilia Manzino, Alberto Pardo |
Agda Formalization of a Security-preserving Translation from Flow-sensitive to Flow-insensitive Security Types. |
LSFA |
2020 |
DBLP DOI BibTeX RDF |
|
24 | Sebastián Urciuoli, Álvaro Tasistro, Nora Szasz |
Strong Normalization for the Simply-Typed Lambda Calculus in Constructive Type Theory Using Agda. |
LSFA |
2020 |
DBLP DOI BibTeX RDF |
|
24 | Luca Ciccone, Luca Padovani |
A Dependently Typed Linear π-Calculus in Agda. |
PPDP |
2020 |
DBLP DOI BibTeX RDF |
|
24 | Niccolò Veltri, Andrea Vezzosi |
Formalizing π-calculus in guarded cubical Agda. |
CPP |
2020 |
DBLP DOI BibTeX RDF |
|
24 | Fredrik Nordvall Forsberg, Chuangjie Xu, Neil Ghani |
Three equivalent ordinal notation systems in cubical Agda. |
CPP |
2020 |
DBLP DOI BibTeX RDF |
|
24 | Andrea Vezzosi, Anders Mörtberg, Andreas Abel 0001 |
Cubical agda: a dependently typed programming language with univalence and higher inductive types. |
Proc. ACM Program. Lang. |
2019 |
DBLP DOI BibTeX RDF |
|
24 | Martín Hötzel Escardó |
Introduction to Univalent Foundations of Mathematics with Agda. |
CoRR |
2019 |
DBLP BibTeX RDF |
|
24 | James Chapman 0001, Roman Kireev, Chad Nester, Philip Wadler |
System F in Agda, for Fun and Profit. |
MPC |
2019 |
DBLP DOI BibTeX RDF |
|
24 | Jesper Cockx |
Type Theory Unchained: Extending Agda with User-Defined Rewrite Rules. |
TYPES |
2019 |
DBLP DOI BibTeX RDF |
|
24 | Niccolò Veltri, Niels van der Weide |
Guarded Recursion in Agda via Sized Types. |
FSCD |
2019 |
DBLP DOI BibTeX RDF |
|
24 | Anton Setzer |
Modelling Bitcoin in Agda. |
CoRR |
2018 |
DBLP BibTeX RDF |
|
24 | Jeremy Pope |
Formalizing Constructive Quantifier Elimination in Agda. |
MSFP@FSCD |
2018 |
DBLP DOI BibTeX RDF |
|
24 | Paventhan Vivekanandan |
Code Generation for Higher Inductive Types - A Study in Agda Metaprogramming. |
WFLP |
2018 |
DBLP DOI BibTeX RDF |
|
24 | Philip Wadler |
Programming Language Foundations in Agda. |
SBMF |
2018 |
DBLP DOI BibTeX RDF |
|
24 | Ran Zmigrod, Matthew L. Daggitt, Timothy G. Griffin |
An Agda Formalization of Üresin and Dubois' Asynchronous Fixed-Point Theory. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
24 | Emmanuel Gunther, Alejandro Gadea, Miguel Pagano |
Formalization of Universal Algebra in Agda. |
LSFA |
2017 |
DBLP DOI BibTeX RDF |
|
24 | Guillermo Calderón |
Formalizing Constructive Projective Geometry in Agda. |
LSFA |
2017 |
DBLP DOI BibTeX RDF |
|
24 | Sergio Antoy, Michael Hanus, Steven Libby |
Proving Non-Deterministic Computations in Agda. |
WLP / WFLP |
2017 |
DBLP DOI BibTeX RDF |
|
24 | Wen Kokke |
Formalising Type-Logical Grammars in Agda. |
CoRR |
2017 |
DBLP BibTeX RDF |
|
24 | Andreas Abel 0001, Stephan Adelsberger, Anton Setzer |
Interactive programming in Agda - Objects and graphical user interfaces. |
J. Funct. Program. |
2017 |
DBLP DOI BibTeX RDF |
|
24 | Bashar Igried, Anton Setzer |
Trace and Stable Failures Semantics for CSP-Agda. |
CoALP-Ty |
2016 |
DBLP DOI BibTeX RDF |
|
24 | Jean-Philippe Bernardy, Patrik Jansson |
Certified Context-Free Parsing: A formalisation of Valiant's Algorithm in Agda. |
Log. Methods Comput. Sci. |
2016 |
DBLP DOI BibTeX RDF |
|
24 | Aaron Stump |
Verified Functional Programming in Agda |
|
2016 |
DOI RDF |
|
24 | Bashar Igried, Anton Setzer |
Defining Trace Semantics for CSP-Agda. |
TYPES |
2016 |
DBLP DOI BibTeX RDF |
|
24 | Adam Sandberg Eriksson, Patrik Jansson |
An agda formalisation of the transitive closure of block matrices (extended abstract). |
TyDe@ICFP |
2016 |
DBLP DOI BibTeX RDF |
|
24 | Pepijn Kokke, Wouter Swierstra |
Auto in Agda - Programming Proof Search Using Reflection. |
MPC |
2015 |
DBLP DOI BibTeX RDF |
|
24 | João Paulo Pizani Flor, Wouter Swierstra, Yorick Sijsling |
Pi-Ware: Hardware Description and Verification in Agda. |
TYPES |
2015 |
DBLP DOI BibTeX RDF |
|
24 | Ernesto Copello, Alvaro Tasistro, Bruno Bianchi |
Case of (Quite) Painless Dependently Typed Programming: Fully Certified Merge Sort in Agda. |
SBLP |
2014 |
DBLP DOI BibTeX RDF |
|
24 | Alan Jeffrey |
Dependently Typed Web Client Applications - FRP in Agda in HTML5. |
PADL |
2013 |
DBLP DOI BibTeX RDF |
|
24 | Christopher Schwaab, Jeremy G. Siek |
Modular type-safety proofs in Agda. |
PLPV |
2013 |
DBLP DOI BibTeX RDF |
|
24 | Paul van der Walt, Wouter Swierstra |
Engineering Proof by Reflection in Agda. |
IFL |
2012 |
DBLP DOI BibTeX RDF |
|
24 | Peter Thiemann 0001, Manuel M. T. Chakravarty |
Agda Meets Accelerate. |
IFL |
2012 |
DBLP DOI BibTeX RDF |
|
24 | Conor Thomas McBride |
Agda-curious?: an exploration of programming with dependent types. |
ICFP |
2012 |
DBLP DOI BibTeX RDF |
|
24 | Karim Kanso |
Agda as a platform for the development of verified railway interlocking systems. |
|
2012 |
RDF |
|
24 | Peter Dybjer, Yoshiki Kinoshita, Shin-Cheng Mu |
Agda Implementors Meeting (NII Shonan Meeting 2011-2). |
NII Shonan Meet. Rep. |
2011 |
DBLP BibTeX RDF |
|
24 | Wouter Swierstra |
Sorted - Verifying the Problem of the Dutch National Flag in Agda. |
J. Funct. Program. |
2011 |
DBLP DOI BibTeX RDF |
|