Agda papers (researchr/bibliography/publications)

researchr

You are not signed in
Sign in
Sign up

Generalized Universe Hierarchies and First-Class Universe LevelsAndrás Kovács. csl 2022: [doi] [classification] 1 years ago

Impredicative Observational EqualityLoïc Pujet, Nicolas Tabareau. PACMPL, 7(POPL):2171-2196, January 2023. [doi] [classification] 1 years ago

Translating Proofs from an Impredicative Type System to a Predicative OneThiago Felicissimo, Frédéric Blanqui, Ashish Kumar Barnawal. csl 2023: [doi] [classification] 1 years ago

Towards a practical programming language based on dependent type theoryUlf Norell. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology, SE-412 96 G\"{o}teborg, Sweden, September 2007. [classification] 1 years ago

Practical dependent type checking using twin typesVíctor López Juan, Nils Anders Danielsson. ICFP 2020: 11-23 [doi] [classification] 1 years ago

Cubical synthetic homotopy theoryAnders Mörtberg, Loïc Pujet. CPP 2020: 158-171 [doi] [classification] 1 years ago

Forward build systems, formallySarah Spall, Neil Mitchell, Sam Tobin-Hochstadt. CPP 2022: 130-142 [doi] [classification] 1 years ago

On homotopy of walks and spherical maps in homotopy type theoryJonathan Prieto-Cubides. CPP 2022: 338-351 [doi] [classification] 1 years ago

First-order natural deduction in AgdaWarren, Louis. 2021. [doi] [classification] 1 years ago

Deeper Shallow EmbeddingsJacob Prinz, G. A. Kavvos, Leonidas Lampropoulos. itp 2022: [doi] [classification] 1 years ago

Constructive Analysis in the Agda Proof AssistantMurray, Zachary. 2022. [doi] [classification] 1 years ago

Representing Agda and coinduction in the $\lambda$$\Pi$-calculus modulo rewritingFelicissimo, Thiago. Master's thesis, LSV, ENS Paris Saclay, Universit{\'e} Paris-Saclay, Sep 2021. [classification] 1 years ago

An approach to translating Haskell programs to Agda and reasoning about themCarr, Harold, Jenkins, Christa, Moir, Mark, Miraldo, Victor Cacciari, Silva, Lisandra. 2022. [doi] [classification] 1 years ago

LibNDT: Towards a Formal Library on Spreadable Properties over Linked Nested DatatypesMathieu Montin, Amélie Ledein, Catherine Dubois. Electronic Proceedings in Theoretical Computer Science, 360:27-44, jun 2022. [doi] [classification] 1 years ago

Teaching automated reasoning and formally verified functional programming in Agda and Isabelle/HOLFrom, Asta Halkjær , Villadsen, Jørgen . In 10th International Workshop on Trends in Functional Programming in Education (TFPIE 2021)--Presentation Only/Online Papers. 2021: 1-20 [classification] 1 years ago

Toward SMT-Based Refinement Types in AgdaShen, Gan, Kuper, Lindsey. 2021. [doi] [classification] 1 years ago

The Agda Universal Algebra Library, Part 1: FoundationDeMeo, William. 2021. [doi] [classification] 1 years ago

Higher-order Games with Dependent TypesEscardo, Martin, Oliva, Paulo. 2022. [doi] [classification] 1 years ago

Sikkel: Multimode Simple Type Theory as an Agda LibraryJoris Ceulemans, Andreas Nuyts, Dominique Devriese. Electronic Proceedings in Theoretical Computer Science, 360:93-112, jun 2022. [doi] [classification] 1 years ago

The Agda Universal Algebra Library, Part 2: StructureDeMeo, William. 2021. [doi] [classification] 1 years ago

Formalizing Affinization of a Projective Plane in AgdaCalderón, Guillermo. In 2021 XLVII Latin American Computing Conference (CLEI). 2021: 1-8 [doi] [classification] 1 years ago

Extracting the power of dependent typesArtjoms Sinkarovs, Jesper Cockx. GPCE 2021: 83-95 [doi] [classification] 1 years ago

A Machine-Checked Proof of Birkhoff's Variety Theorem in Martin-Löf Type TheoryWilliam J. DeMeo, Jacques Carette. TYPES 2022: [doi] [classification] 1 years ago

Formalisation of Dependent Type Theory: The Example of CaTTThibaut Benjamin. TYPES 2022: [doi] [classification] 1 years ago

Elaboration with first-class implicit function typesAndrás Kovács. PACMPL, 4(ICFP), 2020. [doi] [classification] 1 years ago

Asynchronous effectsDanel Ahman, Matija Pretnar. PACMPL, 5(POPL):1-28, 2021. [doi] [classification] 1 years ago

A computational interpretation of compact closed categories: reversible programming with negative and fractional typesChao-Hong Chen, Amr Sabry. PACMPL, 5(POPL):1-29, 2021. [doi] [classification] 1 years ago

The taming of the rew: a type theory with computational assumptionsJesper Cockx, Nicolas Tabareau, Théo Winterhalter. PACMPL, 5(POPL):1-29, 2021. [doi] [classification] 1 years ago

Internalizing representation independence with univalenceCarlo Angiuli, Evan Cavallo, Anders Mörtberg, Max Zeuner. PACMPL, 5(POPL):1-30, 2021. [doi] [classification] 1 years ago

Calculating dependently-typed compilers (functional pearl)Mitchell Pickard, Graham Hutton. PACMPL, 5(ICFP):1-27, 2021. [doi] [classification] 1 years ago

A theory of higher-order subtyping with type intervalsSandro Stucki, Paolo G. Giarrusso. PACMPL, 5(ICFP):1-30, 2021. [doi] [classification] 1 years ago

Algebras for weighted searchDonnacha Oisín Kidney, Nicolas Wu. PACMPL, 5(ICFP):1-30, 2021. [doi] [classification] 1 years ago

A cost-aware logical frameworkYue Niu, Jonathan Sterling, Harrison Grodin, Robert Harper. PACMPL, 6(POPL):1-31, 2022. [doi] [classification] 1 years ago

Observational equality: now for goodLoïc Pujet, Nicolas Tabareau. PACMPL, 6(POPL):1-27, 2022. [doi] [classification] 1 years ago

Formal metatheory of second-order abstract syntaxMarcelo Fiore, Dmitrij Szamozvancev. PACMPL, 6(POPL):1-29, 2022. [doi] [classification] 1 years ago

Plausible sealing for gradual parametricityElizabeth Labrada, Matías Toro, Éric Tanter, Dominique Devriese. PACMPL, 6(OOPSLA):1-28, 2022. [doi] [classification] 1 years ago

Normalization for fitch-style modal calculiNachiappan Valliappan, Fabian Ruch, Carlos Tomé Cortiñas. PACMPL, 6(ICFP):772-798, 2022. [doi] [classification] 1 years ago

Practical generic programming over a universe of native datatypesLucas Escot, Jesper Cockx. PACMPL, 6(ICFP):625-649, 2022. [doi] [classification] 1 years ago

Datatype-generic programming meets elaborator reflectionHsiang-Shang Ko, Liang-Ting Chen, Tzu-Chi Lin. PACMPL, 6(ICFP):225-253, 2022. [doi] [classification] 1 years ago

A completely unique account of enumerationCas van der Rest, Wouter Swierstra. PACMPL, 6(ICFP):411-437, 2022. [doi] [classification] 1 years ago

Intrinsically-typed definitional interpreters à la carteCas van der Rest, Casper Bach Poulsen, Arjen Rouvoet, Eelco Visser, Peter D. Mosses. PACMPL, 6(OOPSLA2):1903-1932, 2022. [doi] [classification] 1 years ago

Type Theory Unchained: Extending Agda with User-Defined Rewrite RulesJesper Cockx. TYPES 2020: [doi] [classification] 1 years ago

Formalizing π-calculus in guarded cubical AgdaNiccolò Veltri, Andrea Vezzosi. CPP 2020: 270-283 [doi] [classification] 1 years ago

Strong Normalization for the Simply-Typed Lambda Calculus in Constructive Type Theory Using AgdaSebastián Urciuoli, Álvaro Tasistro, Nora Szasz. LSFA 2020: 187-203 [doi] [classification] 1 years ago

Intrinsically-typed definitional interpreters for linear, session-typed languagesArjen Rouvoet, Casper Bach Poulsen, Robbert Krebbers, Eelco Visser. CPP 2020: 284-298 [doi] [classification] 1 years ago

A formalisation of LEGv8 in AgdaSantiago Arranz Olmos, Martín-Fernández, Matías Steinberg, Alejandro Gadea, Emmanuel Gunther, Miguel Pagano. SBLP 2020: 33-39 [doi] [classification] 1 years ago

Agda Formalization of a Security-preserving Translation from Flow-sensitive to Flow-insensitive Security TypesCecilia Manzino, Alberto Pardo. LSFA 2020: 75-94 [doi] [classification] 1 years ago

Programming language foundations in AgdaWen Kokke, Jeremy G. Siek, Philip Wadler. SCP, 194:102440, 2020. [doi] [classification] 1 years ago

Encoding Agda Programs Using RewritingGuillaume Genestier. fscd 2020: [doi] [classification] 1 years ago

Three equivalent ordinal notation systems in cubical AgdaFredrik Nordvall Forsberg, Chuangjie Xu, Neil Ghani. CPP 2020: 172-185 [doi] [classification] 1 years ago

A Relaxation of Üresin and Dubois' Asynchronous Fixed-Point Theory in AgdaMatthew L. Daggitt, Ran Zmigrod, Timothy G. Griffin. JAR, 64(5):857-877, 2020. [doi] [classification] 1 years ago

A Dependently Typed Linear π-Calculus in AgdaLuca Ciccone, Luca Padovani. ppdp 2020: [doi] [classification] 1 years ago

π with Leftovers: A Mechanisation in AgdaUma Zalakain, Ornela Dardha. forte 2021: 157-174 [doi] [classification] 1 years ago

Cubical Agda: A dependently typed programming language with univalence and higher inductive typesAndrea Vezzosi, Anders Mörtberg, Andreas Abel 0001. JFP, 31, 2021. [doi] [classification] 1 years ago

Intrinsically typed compilation with nameless labelsArjen Rouvoet, Robbert Krebbers, Eelco Visser. PACMPL, 5(POPL):1-28, 2021. [doi] [classification] 1 years ago

Formal verification of authenticated, append-only skip lists in AgdaVictor Cacciari Miraldo, Harold Carr, Mark Moir, Lisandra Silva, Guy L. Steele Jr.. CPP 2021: 122-136 [doi] [classification] 1 years ago

Formalizing category theory in AgdaJason Z. S. Hu, Jacques Carette. CPP 2021: 327-342 [doi] [classification] 1 years ago

Towards an Extrinsic Formalization of Featherweight Java in AgdaSamuel da Silva Feitosa, Rodrigo Geraldo Ribeiro, André Rauber Du Bois. cleiej, 24(3), 2021. [doi] [classification] 1 years ago

Flexible Coinduction in AgdaLuca Ciccone, Francesco Dagnino, Elena Zucca. itp 2021: [doi] [classification] 1 years ago

Verification of Bitcoin Script in Agda Using Weakest Preconditions for Access ControlFahad F. Alhabardi, Arnold Beckmann, Bogdan Lazar, Anton Setzer. TYPES 2022: [doi] [classification] 1 years ago

Towards Formal Verification of HotStuff-Based Byzantine Fault Tolerant Consensus in AgdaHarold Carr, Christa Jenkins, Mark Moir, Victor Cacciari Miraldo, Lisandra Silva. NFM 2022: 616-635 [doi] [classification] 1 years ago

Synthetic Integral Cohomology in Cubical AgdaGuillaume Brunerie, Axel Ljungström, Anders Mörtberg. csl 2022: [doi] [classification] 1 years ago

Reasonable Agda is correct Haskell: writing verified Haskell using agda2hsJesper Cockx, Orestis Melkonian, Lucas Escot, James Chapman, Ulf Norell. haskell 2022: 108-122 [doi] [classification] 1 years ago

Refinement types and computational dualityNoam Zeilberger. plpv 2009: 15-26 [doi] [classification] 4 years ago

Focusing and higher-order abstract syntaxNoam Zeilberger. POPL 2008: 359-369 [doi] [classification] 4 years ago

A continuous computational interpretation of type theoriesChuangjie Xu. PhD thesis, University of Birmingham, UK, 2015. [doi] [classification] 4 years ago

A Constructive Model of Uniform ContinuityChuangjie Xu, Martín Hötzel Escardó. tlca 2013: 236-249 [doi] [classification] 4 years ago

Two set-based implementations of quotients in type theoryNiccolò Veltri. splst 2015: 194-205 [doi] [classification] 4 years ago

From fine- to coarse-grained dynamic information flow control and backMarco Vassena, Alejandro Russo, Deepak Garg, Vineet Rajani, Deian Stefan. PACMPL, 3, 2019. [doi] [classification] 4 years ago

On Formalizing Information-Flow Control LibrariesMarco Vassena, Alejandro Russo. ccs 2016: 15-28 [doi] [classification] 4 years ago

The Sequent Calculus of Skew Monoidal CategoriesTarmo Uustalu, Niccolò Veltri, Noam Zeilberger. ENTCS, 341:345-370, 2018. [doi] [classification] 4 years ago

The Delay Monad and Restriction CategoriesTarmo Uustalu, Niccolò Veltri. ictac 2017: 32-50 [doi] [classification] 4 years ago

Partiality and Container MonadsTarmo Uustalu, Niccolò Veltri. aplas 2017: 406-425 [doi] [classification] 4 years ago

Finiteness and rational sequences, constructivelyTarmo Uustalu, Niccolò Veltri. JFP, 27, 2017. [doi] [classification] 4 years ago

From algebra to abstract machine: a verified generic constructionCarlos Tomé Cortiñas, Wouter Swierstra. ICFP 2018: 78-90 [doi] [classification] 4 years ago

Formalisation in Constructive Type Theory of Stoughton's Substitution for the Lambda CalculusAlvaro Tasistro, Ernesto Copello, Nora Szasz. ENTCS, 312:215-230, 2015. [doi] [classification] 4 years ago

A library for polymorphic dynamic typingWouter Swierstra, Thomas van Noort. JFP, 23(3):229-248, 2013. [doi] [classification] 4 years ago

Dependent Types for Distributed ArraysWouter Swierstra, Thorsten Altenkirch. sfp 2008: 17-32 [classification] 4 years ago

More dependent types for distributed arraysWouter Swierstra. lisp, 23(4):489-506, 2010. [doi] [classification] 4 years ago

Generic programming of all kindsAlejandro Serrano, Victor Cacciari Miraldo. haskell 2018: 41-54 [doi] [classification] 4 years ago

Work it, wrap it, fix it, fold itNeil Sculthorpe, Graham Hutton. JFP, 24(1):113-127, 2014. [doi] [classification] 4 years ago

A fresh look at programming with names and bindersNicolas Pouillard, François Pottier. ICFP 2010: 217-228 [doi] [classification] 4 years ago

Nameless, painlessNicolas Pouillard. ICFP 2011: 320-332 [doi] [classification] 4 years ago

Namely, Painless: A unifying approach to safe programming with first-order syntax with binders. (Une approche unifiante pour programmer sûrement avec de la syntaxe du premier ordre contenant des lieurs)Nicolas Pouillard. PhD thesis, Paris Diderot University, France, 2012. [doi] [classification] 4 years ago

The power of PiNicolas Oury, Wouter Swierstra. ICFP 2008: 39-50 [doi] [classification] 4 years ago

Axioms for Modelling Cubical Type Theory in a ToposIan Orton, Andrew M. Pitts. lmcs, 14(4), 2018. [doi] [classification] 4 years ago

Axioms for Modelling Cubical Type Theory in a ToposIan Orton, Andrew M. Pitts. csl 2016: [doi] [classification] 4 years ago

Decomposing the Univalence AxiomIan Orton, Andrew M. Pitts. TYPES 2018: [doi] [classification] 4 years ago

Hazelnut: a bidirectionally typed structure editor calculusCyrus Omar, Ian Voysey, Michael Hilton, Jonathan Aldrich, Matthew A. Hammer. POPL 2017: 86-99 [doi] [classification] 4 years ago

Deferring the details and deriving programsLiam O'Connor. ICFP 2019: 27-39 [doi] [classification] 4 years ago

Applications of applicative proof searchLiam O'Connor. ICFP 2016: 43-55 [doi] [classification] 4 years ago

Interactive programming with dependent typesUlf Norell. ICFP 2013: 1-2 [doi] [classification] 4 years ago

Embedding polymorphic dynamic typingThomas van Noort, Wouter Swierstra, Peter Achten, Rinus Plasmeijer. ICFP 2011: 25-36 [doi] [classification] 4 years ago

Algebra of Programming Using Dependent TypesShin-Cheng Mu, Hsiang-Shang Ko, Patrik Jansson. mpc 2008: 268-283 [doi] [classification] 4 years ago

Security-typed programming within dependently typed programmingJamie Morgenstern, Daniel R. Licata. ICFP 2010: 169-180 [doi] [classification] 4 years ago

Turing-Completeness Totally FreeConor McBride. mpc 2015: 257-275 [doi] [classification] 4 years ago

Outrageous but meaningful coincidences: dependent type-safe syntax and evaluationConor McBride. ICFP 2010: 1-12 [doi] [classification] 4 years ago

How to keep your neighbours in orderConor Thomas McBride. ICFP 2014: 297-309 [doi] [classification] 4 years ago

Djinn, MonotonicConor McBride. itp 2012: 14-17 [doi] [classification] 4 years ago

Certified normalization of generalized tracesHendrik Maarand, Tarmo Uustalu. isse, 15(3-4):253-265, 2019. [doi] [classification] 4 years ago

runs on WebDSL