Search results for "agda"

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