Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
101 | Ulf Norell |
Dependently typed programming in Agda. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TLDI ![In: Proceedings of TLDI'09: 2009 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Savannah, GA, USA, January 24, 2009, pp. 1-2, 2009, ACM, 978-1-60558-420-1. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, pp. 73-78, 2009, Springer, 978-3-642-03358-2. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
82 | Ana Bove, Peter Dybjer, Andrés Sicard-Ramírez |
Embedding a logical theory of constructions in Agda. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PLPV ![In: Proceedings of the 3rd ACM Workshop Programming Languages meets Program Verification, PLPV 2009, Savannah, GA, USA, January 20, 2009, pp. 59-66, 2009, ACM, 978-1-60558-330-3. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: Types for Proofs and Programs, International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, 2004, Revised Selected Papers, pp. 154-169, 2004, Springer, 3-540-31428-8. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Haskell ![In: Proceedings of the ACM SIGPLAN Workshop on Haskell, Haskell 2005, Tallinn, Estonia, September 30, 2005, pp. 62-73, 2005, ACM, 1-59593-071-X. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
GHC core, monadic translation, verification, haskell, type theory, partiality |
58 | Ana Bove, Peter Dybjer |
Dependent Types at Work. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LerNet ALFA Summer School ![In: Language Engineering and Rigorous Software Development, International LerNet ALFA Summer School 2008, Piriapolis, Uruguay, February 24 - March 1, 2008, Revised Tutorial Lectures, pp. 57-99, 2008, Springer, 978-3-642-03152-6. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
52 | Stephanie Weirich, Chris Casinghino |
Arity-generic datatype-generic programming. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PLPV ![In: Proceedings of the 4th ACM Workshop Programming Languages meets Program Verification, PLPV 2010, Madrid, Spain, January 19, 2010, pp. 15-26, 2010, ACM, 978-1-60558-890-2. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
agda, arity-generic programming, generic haskell, dependent types |
52 | Daniel R. Licata, Robert Harper 0001 |
Positively dependent types. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PLPV ![In: Proceedings of the 3rd ACM Workshop Programming Languages meets Program Verification, PLPV 2009, Savannah, GA, USA, January 20, 2009, pp. 3-14, 2009, ACM, 978-1-60558-330-3. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2307.10455, 2023. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
NeurIPS ![In: Advances in Neural Information Processing Systems 36: Annual Conference on Neural Information Processing Systems 2023, NeurIPS 2023, New Orleans, LA, USA, December 10 - 16, 2023., 2023. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Comput. Electron. Agric. ![In: Comput. Electron. Agric. 196, pp. 106877, 2022. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
HCI (17) ![In: Digital Human Modeling and Applications in Health, Safety, Ergonomics and Risk Management. Healthcare Applications - 10th International Conference, DHM 2019, Held as Part of the 21st HCI International Conference, HCII 2019, Orlando, FL, USA, July 26-31, 2019, Proceedings, Part II, pp. 209-221, 2019, Springer, 978-3-030-22218-5. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
41 | Veridianna Cristina Teodoro Ferreira, Agda Carvalho |
Inclusive Design and Textile Technology in the Everyday Lives of Wheelchair Dependent. ![Search on Bibsonomy](Pics/bibsonomy.png) |
HCI (17) ![In: Digital Human Modeling. Applications in Health, Safety, Ergonomics, and Risk Management - 9th International Conference, DHM 2018, Held as Part of HCI International 2018, Las Vegas, NV, USA, July 15-20, 2018, Proceedings, pp. 295-307, 2018, Springer, 978-3-319-91396-4. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
HCI (21) ![In: Distributed, Ambient and Pervasive Interactions - 5th International Conference, DAPI 2017, Held as Part of HCI International 2017, Vancouver, BC, Canada, July 9-14, 2017, Proceedings, pp. 547-560, 2017, Springer, 978-3-319-58696-0. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Bioinform. ![In: Bioinform. 30(8), pp. 1073-1080, 2014. The full citation details ...](Pics/full.jpeg) |
2014 |
DBLP DOI BibTeX RDF |
|
39 | Noam Zeilberger |
Refinement types and computational duality. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PLPV ![In: Proceedings of the 3rd ACM Workshop Programming Languages meets Program Verification, PLPV 2009, Savannah, GA, USA, January 20, 2009, pp. 15-26, 2009, ACM, 978-1-60558-330-3. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
duality, effects, intersection types, focusing, union types |
39 | Neil Sculthorpe, Henrik Nilsson |
Safe functional reactive programming through dependent types. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICFP ![In: Proceeding of the 14th ACM SIGPLAN international conference on Functional programming, ICFP 2009, Edinburgh, Scotland, UK, August 31 - September 2, 2009, pp. 23-34, 2009, ACM, 978-1-60558-332-7. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
VSTTE ![In: Verified Software: Theories, Tools, Experiments, Second International Conference, VSTTE 2008, Toronto, Canada, October 6-9, 2008. Proceedings, pp. 115-129, 2008, Springer, 978-3-540-87872-8. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
39 | Peter Dybjer, Qiao Haiyan, Makoto Takeyama |
Combining Testing and Proving in Dependent Type Theory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 16th International Conference, TPHOLs 2003, Rom, Italy, September 8-12, 2003, Proceedings, pp. 188-203, 2003, Springer, 3-540-40664-6. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
24 | Donnacha Oisín Kidney, Zhixuan Yang, Nicolas Wu |
Algebraic Effects Meet Hoare Logic in Cubical Agda. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Proc. ACM Program. Lang. ![In: Proc. ACM Program. Lang. 8(POPL), pp. 1663-1695, January 2024. The full citation details ...](Pics/full.jpeg) |
2024 |
DBLP DOI BibTeX RDF |
|
24 | Antoine Van Muylder, Andreas Nuyts, Dominique Devriese |
Internal and Observational Parametricity for Cubical Agda. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Proc. ACM Program. Lang. ![In: Proc. ACM Program. Lang. 8(POPL), pp. 209-240, January 2024. The full citation details ...](Pics/full.jpeg) |
2024 |
DBLP DOI BibTeX RDF |
|
24 | Maximilian Doré, Evan Cavallo, Anders Mörtberg |
Automating Boundary Filling in Cubical Agda. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2402.12169, 2024. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Aspects Comput. ![In: Formal Aspects Comput. 36(1), pp. 7:1-7:2, March 2024. The full citation details ...](Pics/full.jpeg) |
2024 |
DBLP DOI BibTeX RDF |
|
24 | Cosmo Viola, Max Fan, Talia Ringer |
Towards Proof Repair in Cubical Agda. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2310.06959, 2023. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2302.00151, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
24 | Niccolò Veltri, Andrea Vezzosi |
Formalizing CCS and π-calculus in Guarded Cubical Agda. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Log. Algebraic Methods Program. ![In: J. Log. Algebraic Methods Program. 131, pp. 100846, February 2023. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LICS ![In: LICS, pp. 1-13, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
24 | Fahad F. Alhabardi, Anton Setzer |
A model of Solidity-style smart contracts in the theorem prover Agda. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AIBThings ![In: IEEE International Conference on Artificial Intelligence, Blockchain, and Internet of Things, AIBThings 2023, Mount Pleasant, MI, USA, September 16-17, 2023, pp. 1-10, 2023, IEEE, 979-8-3503-2234-7. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
24 | Thomas Lamiaux, Axel Ljungström, Anders Mörtberg |
Computing Cohomology Rings in Cubical Agda. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, Boston, MA, USA, January 16-17, 2023, pp. 239-252, 2023, ACM. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
24 | Joris Ceulemans, Andreas Nuyts, Dominique Devriese |
Sikkel: Multimode Simple Type Theory as an Agda Library. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MSFP@ETAPS ![In: Proceedings Ninth Workshop on Mathematically Structured Functional Programming, MSFP@ETAPS 2022, Munich, Germany, 2nd April 2022., pp. 93-112, 2022. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2203.14711, 2022. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2203.03054, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
24 | Sebastián Urciuoli |
A Formal Proof of the Strong Normalization Theorem for System T in Agda. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LSFA ![In: Proceedings 17th International Workshop on Logical and Semantic Frameworks with Applications, LSFA 2022, Belo Horizonte, Brazil (hybrid), 23-24 September 2022., pp. 81-99, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
24 | Thomas Lamiaux, Axel Ljungström, Anders Mörtberg |
Computing Cohomology Rings in Cubical Agda. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2212.04182, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
24 | Zachary Murray |
Constructive Analysis in the Agda Proof Assistant. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2205.08354, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
24 | Miguel Pagano, José E. Solsona |
Nominal Sets in Agda - A Fresh and Immature Mechanization. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LSFA ![In: Proceedings 17th International Workshop on Logical and Semantic Frameworks with Applications, LSFA 2022, Belo Horizonte, Brazil (hybrid), 23-24 September 2022., pp. 67-80, 2022. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2205.08718, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
24 | Stephen Dolan |
Computing with generic trees in Agda. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TyDe@ICFP ![In: TyDe '22: 7th ACM SIGPLAN International Workshop on Type-Driven Development, Ljubljana, Slovenia, 11 September 2022, pp. 38-44, 2022, ACM, 978-1-4503-9439-0. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
NFM ![In: NASA Formal Methods - 14th International Symposium, NFM 2022, Pasadena, CA, USA, May 24-27, 2022, Proceedings, pp. 616-635, 2022, Springer, 978-3-031-06772-3. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
24 | Guillaume Brunerie, Axel Ljungström, Anders Mörtberg |
Synthetic Integral Cohomology in Cubical Agda. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CSL ![In: 30th EACSL Annual Conference on Computer Science Logic, CSL 2022, February 14-19, 2022, Göttingen, Germany (Virtual Conference)., pp. 11:1-11:19, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-218-1. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Haskell ![In: Haskell '22: 15th ACM SIGPLAN International Haskell Symposium, Ljubljana, Slovenia, September 15 - 16, 2022, pp. 108-122, 2022, ACM, 978-1-4503-9438-3. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CLEI Electron. J. ![In: CLEI Electron. J. 24(3), 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
24 | William J. DeMeo |
The Agda Universal Algebra Library, Part 1: Foundation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2103.05581, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP BibTeX RDF |
|
24 | William J. DeMeo |
The Agda Universal Algebra Library, Part 2: Structure. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2103.09092, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP BibTeX RDF |
|
24 | Gan Shen, Lindsey Kuper |
Toward SMT-Based Refinement Types in Agda. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2110.05771, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP BibTeX RDF |
|
24 | Andreas Abel 0001 |
Birkhoff's Completeness Theorem for Multi-Sorted Algebras Formalized in Agda. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2111.07936, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP BibTeX RDF |
|
24 | William J. DeMeo |
The Agda Universal Algebra Library and Birkhoff's Theorem in Martin-Löf Dependent Type Theory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2101.10166, 2021. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2103.04519, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP BibTeX RDF |
|
24 | Louis Warren |
First-order natural deduction in Agda. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2104.04095, 2021. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Funct. Program. ![In: J. Funct. Program. 31, pp. e8, 2021. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 27th International Conference on Types for Proofs and Programs, TYPES 2021, June 14-18, 2021, Leiden, The Netherlands (Virtual Conference)., pp. 1:1-1:25, 2021, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-254-9. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
24 | Guillermo Calderón |
Formalizing Affinization of a Projective Plane in Agda. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CLEI ![In: XLVII Latin American Computing Conference, CLEI 2021, Cartago, Costa Rica, October 25-29, 2021, pp. 1-8, 2021, IEEE, 978-1-6654-9503-5. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
24 | Luca Ciccone, Francesco Dagnino, Elena Zucca |
Flexible Coinduction in Agda. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)., pp. 13:1-13:19, 2021, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-188-7. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021, pp. 122-136, 2021, ACM, 978-1-4503-8299-1. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
24 | Jason Z. S. Hu, Jacques Carette |
Formalizing category theory in Agda. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021, pp. 327-342, 2021, ACM, 978-1-4503-8299-1. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
24 | Uma Zalakain, Ornela Dardha |
π with Leftovers: A Mechanisation in Agda. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FORTE ![In: Formal Techniques for Distributed Objects, Components, and Systems - 41st IFIP WG 6.1 International Conference, FORTE 2021, Held as Part of the 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021, Valletta, Malta, June 14-18, 2021, Proceedings, pp. 157-174, 2021, Springer, 978-3-030-78088-3. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
24 | Jason Z. S. Hu, Jacques Carette |
Proof-relevant Category Theory in Agda. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2005.07059, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP BibTeX RDF |
|
24 | Uma Zalakain, Ornela Dardha |
π with leftovers: a mechanisation in Agda. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2005.05902, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP BibTeX RDF |
|
24 | Pierre Lescanne |
Extensive Infinite Games and Escalation, an exercise in Agda. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2006.15137, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP BibTeX RDF |
|
24 | Luca Ciccone |
Flexible Coinduction in Agda. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2002.06047, 2020. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 64(5), pp. 857-877, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
24 | Wen Kokke, Jeremy G. Siek, Philip Wadler |
Programming language foundations in Agda. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Sci. Comput. Program. ![In: Sci. Comput. Program. 194, pp. 102440, 2020. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SBLP ![In: SBLP '20: 24th Brazilian Symposium on Programming Languages, Natal, Rio Grande do Norte, Brazil, October 19-23, 2020, pp. 33-39, 2020, ACM, 978-1-4503-8943-3. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
24 | Guillaume Genestier |
Encoding Agda Programs Using Rewriting. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FSCD ![In: 5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020, June 29-July 6, 2020, Paris, France (Virtual Conference)., pp. 31:1-31:17, 2020, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-155-9. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LSFA ![In: Proceedings of the 15th International Workshop on Logical and Semantic Frameworks with Applications, LSFA 2020, Online, September 15, 2020, pp. 75-94, 2020, Elsevier. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LSFA ![In: Proceedings of the 15th International Workshop on Logical and Semantic Frameworks with Applications, LSFA 2020, Online, September 15, 2020, pp. 187-203, 2020, Elsevier. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
24 | Luca Ciccone, Luca Padovani |
A Dependently Typed Linear π-Calculus in Agda. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PPDP ![In: PPDP '20: 22nd International Symposium on Principles and Practice of Declarative Programming, Bologna, Italy, 9-10 September, 2020, pp. 8:1-8:14, 2020, ACM, 978-1-4503-8821-4. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
24 | Niccolò Veltri, Andrea Vezzosi |
Formalizing π-calculus in guarded cubical Agda. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020., pp. 270-283, 2020, ACM, 978-1-4503-7097-4. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
24 | Fredrik Nordvall Forsberg, Chuangjie Xu, Neil Ghani |
Three equivalent ordinal notation systems in cubical Agda. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020., pp. 172-185, 2020, ACM, 978-1-4503-7097-4. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Proc. ACM Program. Lang. ![In: Proc. ACM Program. Lang. 3(ICFP), pp. 87:1-87:29, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
24 | Martín Hötzel Escardó |
Introduction to Univalent Foundations of Mathematics with Agda. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1911.00580, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP BibTeX RDF |
|
24 | James Chapman 0001, Roman Kireev, Chad Nester, Philip Wadler |
System F in Agda, for Fun and Profit. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MPC ![In: Mathematics of Program Construction - 13th International Conference, MPC 2019, Porto, Portugal, October 7-9, 2019, Proceedings, pp. 255-297, 2019, Springer, 978-3-030-33635-6. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
24 | Jesper Cockx |
Type Theory Unchained: Extending Agda with User-Defined Rewrite Rules. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 25th International Conference on Types for Proofs and Programs, TYPES 2019, June 11-14, 2019, Oslo, Norway., pp. 2:1-2:27, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-158-0. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
24 | Niccolò Veltri, Niels van der Weide |
Guarded Recursion in Agda via Sized Types. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FSCD ![In: 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, June 24-30, 2019, Dortmund, Germany., pp. 32:1-32:19, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-107-8. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
24 | Anton Setzer |
Modelling Bitcoin in Agda. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1804.06398, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP BibTeX RDF |
|
24 | Jeremy Pope |
Formalizing Constructive Quantifier Elimination in Agda. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MSFP@FSCD ![In: Proceedings of the 7th Workshop on Mathematically Structured Functional Programming, MSFP@FSCD 2018, Oxford, UK, 8th July 2018., pp. 2-17, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
24 | Paventhan Vivekanandan |
Code Generation for Higher Inductive Types - A Study in Agda Metaprogramming. ![Search on Bibsonomy](Pics/bibsonomy.png) |
WFLP ![In: Functional and Constraint Logic Programming - 26th International Workshop, WFLP 2018, Frankfurt/Main, Germany, September 6, 2018, Revised Selected Papers, pp. 18-35, 2018, Springer, 978-3-030-16201-6. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
24 | Philip Wadler |
Programming Language Foundations in Agda. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SBMF ![In: Formal Methods: Foundations and Applications - 21st Brazilian Symposium, SBMF 2018, Salvador, Brazil, November 26-30, 2018, Proceedings, pp. 56-73, 2018, Springer, 978-3-030-03043-8. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings, pp. 623-639, 2018, Springer, 978-3-319-94820-1. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
24 | Emmanuel Gunther, Alejandro Gadea, Miguel Pagano |
Formalization of Universal Algebra in Agda. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LSFA ![In: 12th Workshop on Logical and Semantic Frameworks, with Applications, LSFA 2017, Brasília, Brazil, September 23-24, 2017, pp. 147-166, 2017, Elsevier. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
24 | Guillermo Calderón |
Formalizing Constructive Projective Geometry in Agda. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LSFA ![In: 12th Workshop on Logical and Semantic Frameworks, with Applications, LSFA 2017, Brasília, Brazil, September 23-24, 2017, pp. 61-77, 2017, Elsevier. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
24 | Sergio Antoy, Michael Hanus, Steven Libby |
Proving Non-Deterministic Computations in Agda. ![Search on Bibsonomy](Pics/bibsonomy.png) |
WLP / WFLP ![In: Proceedings 29th and 30th Workshops on (Constraint) Logic Programming and 24th International Workshop on Functional and (Constraint) Logic Programming, WLP 2015 / WLP 2016 / WFLP 2016, Dresden and Leipzig, Germany, 22nd September 2015 and 12-14th September 2016., pp. 180-195, 2017. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
24 | Wen Kokke |
Formalising Type-Logical Grammars in Agda. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1709.00728, 2017. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP BibTeX RDF |
|
24 | Andreas Abel 0001, Stephan Adelsberger, Anton Setzer |
Interactive programming in Agda - Objects and graphical user interfaces. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Funct. Program. ![In: J. Funct. Program. 27, pp. e8, 2017. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
24 | Bashar Igried, Anton Setzer |
Trace and Stable Failures Semantics for CSP-Agda. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoALP-Ty ![In: Proceedings of the First Workshop on Coalgebra, Horn Clause Logic Programming and Types, CoALP-Ty 2016, Edinburgh, UK, 28-29 November 2016., pp. 36-51, 2016. The full citation details ...](Pics/full.jpeg) |
2016 |
DBLP DOI BibTeX RDF |
|
24 | Jean-Philippe Bernardy, Patrik Jansson |
Certified Context-Free Parsing: A formalisation of Valiant's Algorithm in Agda. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Log. Methods Comput. Sci. ![In: Log. Methods Comput. Sci. 12(2), 2016. The full citation details ...](Pics/full.jpeg) |
2016 |
DBLP DOI BibTeX RDF |
|
24 | Aaron Stump |
Verified Functional Programming in Agda ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
2016 |
DOI RDF |
|
24 | Bashar Igried, Anton Setzer |
Defining Trace Semantics for CSP-Agda. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 22nd International Conference on Types for Proofs and Programs, TYPES 2016, May 23-26, 2016, Novi Sad, Serbia, pp. 12:1-12:23, 2016, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-065-1. The full citation details ...](Pics/full.jpeg) |
2016 |
DBLP DOI BibTeX RDF |
|
24 | Adam Sandberg Eriksson, Patrik Jansson |
An agda formalisation of the transitive closure of block matrices (extended abstract). ![Search on Bibsonomy](Pics/bibsonomy.png) |
TyDe@ICFP ![In: Proceedings of the 1st International Workshop on Type-Driven Development, TyDe@ICFP 2016, Nara, Japan, September 18, 2016, pp. 60-61, 2016, ACM, 978-1-4503-4435-7. The full citation details ...](Pics/full.jpeg) |
2016 |
DBLP DOI BibTeX RDF |
|
24 | Pepijn Kokke, Wouter Swierstra |
Auto in Agda - Programming Proof Search Using Reflection. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MPC ![In: Mathematics of Program Construction - 12th International Conference, MPC 2015, Königswinter, Germany, June 29 - July 1, 2015. Proceedings, pp. 276-301, 2015, Springer, 978-3-319-19796-8. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
24 | João Paulo Pizani Flor, Wouter Swierstra, Yorick Sijsling |
Pi-Ware: Hardware Description and Verification in Agda. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 21st International Conference on Types for Proofs and Programs, TYPES 2015, May 18-21, 2015, Tallinn, Estonia, pp. 9:1-9:27, 2015, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-030-9. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SBLP ![In: Programming Languages - 18th Brazilian Symposium, SBLP 2014, Maceio, Brazil, October 2-3, 2014. Proceedings, pp. 62-76, 2014, Springer, 978-3-319-11862-8. The full citation details ...](Pics/full.jpeg) |
2014 |
DBLP DOI BibTeX RDF |
|
24 | Alan Jeffrey |
Dependently Typed Web Client Applications - FRP in Agda in HTML5. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PADL ![In: Practical Aspects of Declarative Languages - 15th International Symposium, PADL 2013, Rome, Italy, January 21-22, 2013. Proceedings, pp. 228-243, 2013, Springer, 978-3-642-45283-3. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
24 | Christopher Schwaab, Jeremy G. Siek |
Modular type-safety proofs in Agda. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PLPV ![In: Proceedings of the 7th Workshop on Programming languages meets program verification, PLPV 2013, Rome, Italy, January 22, 2013, pp. 3-12, 2013, ACM, 978-1-4503-1860-0. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
24 | Paul van der Walt, Wouter Swierstra |
Engineering Proof by Reflection in Agda. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IFL ![In: Implementation and Application of Functional Languages - 24th International Symposium, IFL 2012, Oxford, UK, August 30 - September 1, 2012, Revised Selected Papers, pp. 157-173, 2012, Springer, 978-3-642-41581-4. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
24 | Peter Thiemann 0001, Manuel M. T. Chakravarty |
Agda Meets Accelerate. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IFL ![In: Implementation and Application of Functional Languages - 24th International Symposium, IFL 2012, Oxford, UK, August 30 - September 1, 2012, Revised Selected Papers, pp. 174-189, 2012, Springer, 978-3-642-41581-4. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
24 | Conor Thomas McBride |
Agda-curious?: an exploration of programming with dependent types. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICFP ![In: ACM SIGPLAN International Conference on Functional Programming, ICFP'12, Copenhagen, Denmark, September 9-15, 2012, pp. 1-2, 2012, ACM, 978-1-4503-1054-3. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
24 | Karim Kanso |
Agda as a platform for the development of verified railway interlocking systems. ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
2012 |
RDF |
|
24 | Peter Dybjer, Yoshiki Kinoshita, Shin-Cheng Mu |
Agda Implementors Meeting (NII Shonan Meeting 2011-2). ![Search on Bibsonomy](Pics/bibsonomy.png) |
NII Shonan Meet. Rep. ![In: NII Shonan Meet. Rep. 2011, 2011. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP BibTeX RDF |
|
24 | Wouter Swierstra |
Sorted - Verifying the Problem of the Dutch National Flag in Agda. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Funct. Program. ![In: J. Funct. Program. 21(6), pp. 573-583, 2011. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|