The Idris Language

• Idris 2: Quantitative Type Theory in Practice, Edwin Brady. 2021. In 35th European Conference on Object-Oriented Programming (ECOOP 2021). DOI: 10.4230/LIPIcs.ECOOP.2021.9.
• Idris, a General Purpose Dependently Typed Programming Language: Design and Implementation, Edwin Brady. 2013. In Journal of Functional Programming (JFP). DOI: 10.1017/S095679681300018X.

Associated Publications

There are numerous academic publications associated with Idris, some of which are listed below. If we have missed one or new ones have been published, please do submit a pull request.

• Frex: Dependently Typed Algebraic Simplification, Guillaume Allais, Edwin Brady, Nathan Corbyn, Ohad Kammar, and Jeremy Yallop. 2025. Proceedings of the ACM on Programming Languages, Volume 9, Issue International Conference on Functional Programming (ICFP) (August 2025). DOI: 10.1145/3747506.
• Towards Coherent Semantics: A Quantitatively Typed EDSL for Synchronous System Design, Rui Chen and Ingo Sander. 2025. Design, Automation & Test in Europe Conference (DATE). DOI: 10.23919/DATE64628.2025.10992876.
• Towards being positively negative about dependent types, Jan de Muijnck-Hughes. 2025. Extended Abstract Presented at the 31st Conference on Types for Proofs and Programs.
• A Quantitative Type Approach to Formal Component-Based System Design, Rui Chen and Ingo Sander. 2024. In Forum on Specification & Design Languages (FDL). DOI: 10.1109/FDL63219.2024.10673844.
• Type-Level Property Based Testing, Thomas Ekström Hansen and Edwin Brady. 2024. In Proceedings of the 9th ACM SIGPLAN International Workshop on Type-Driven Development (TyDe 2024). DOI: 10.1145/3678000.3678206.
• Dependent Types to Push Corners of the Property-based Testing, Denis Buzdalov. 2024. Extended Abstract Presented at the 9th ACM SIGPLAN International Workshop on Type-Driven Development (TyDe 2024).
• Colouring flags with Dafny & Idris, Jan de Muijnck-Hughes and James Noble. 2024. Paper presented at Dafny 2024.
• Wiring Circuits Is Easy as {0,1,ω}, or Is It..., Jan de Muijnck-Hughes and Wim Vanderbauwhede. 2023. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). DOI: 10.4230/LIPIcs.ECOOP.2023.8.
• Builtin Types Viewed as Inductive Families, Guillaume Allais. 2023. In Proceedings of the 32nd European Symposium on Programming (ESOP 2023). DOI: 10.1007/978-3-031-30044-8_5.
• Type-safe Quantum Programming in Idris, Liliane-Joy Dandy, Emmanuel Jeandel, and Vladimir Zamdzhiev. 2023. In Proceedings of the 32nd European Symposium on Programming (ESOP 2023). DOI: 10.1007/978-3-031-30044-8_19.
• Type Theory as a Language Workbench, Jan de Muijnck-Hughes, Guillaume Allais, and Edwin Brady. 2023. In Eelco Visser Commemorative Symposium (EVCS 2023). DOI: 10.4230/OASIcs.EVCS.2023.9.
• Dependent tagless final, Nicolas Biri. 2022. In Proceedings of the 2022 ACM SIGPLAN International Workshop on Partial Evaluation and Program Manipulation (PEPM 2022). DOI: 10.1145/3498886.3502201.
• A Typing Discipline for Hardware Interfaces, Jan de Muijnck-Hughes and Wim Vanderbauwhede. 2019. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). DOI: 10.4230/LIPIcs.ECOOP.2019.6.
• Building a Blockchain Simulation using the Idris Programming Language, Qiutai Pan and Xenofon Koutsoukos. 2019. In Proceedings of the 2019 ACM Southeast Conference (ACMSE '19). DOI: 10.1145/3299815.3314456.
• Value Dependent Session Design in a Dependently Typed Language, Jan de Muijnck-Hughes, Wim Vanderbauwhede, and Edwin Brady. 2019. In Proceedings of Programming Language Approaches to Concurrency- and Communication-cEntric Software (PLACES) 2019. DOI: 10.4204/EPTCS.291.5.
• Typing, representing, and abstracting control: functional pearl, Philipp Schuster and Jonathan Immanuel Brachthäuser. 2018. In Proceedings of the 3rd ACM SIGPLAN International Workshop on Type-Driven Development (TyDe 2018). doi: 10.1145/3240719.3241788.
• Automatically Proving Equivalence by Type-Safe Reflection, Franck Slama and Edwin Brady. 2017. In Conference on Intelligent Computer Mathematics (CICM) 2017. DOI: 10.1007/978-3-319-62075-6_4.
• Type-driven Development of Concurrent Communicating Systems, Edwin Brady. 2017. Computer Science Journal (CSCI). AGH University of Science and Technology. DOI: 10.7494/csci.2017.18.3.1413.
• Elaboration Reflection: Extending Idris in Idris, David Christiansen and Edwin Brady. 2016. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (ICFP 2016). DOI: 10.1145/2951913.2951932.
• Resource-dependent Algebraic Effects, Edwin Brady. 2014. In Proceedings of Trends in Functional Programming (TFP). DOI: 10.1007/978-3-319-14675-1_2.
• Dependent Type Providers, David Christiansen. 2013. In Proceedings of the 9th ACM SIGPLAN workshop on Generic Programming (WGP '13). DOI: 10.1145/2502488.2502495.
• Dependent Types for Safe and Secure Web Programming, Simon Fowler and Edwin Brady. 2013. In Proceedings of the 25th symposium on Implementation and Application of Functional Languages (IFL '13). DOI: 10.1145/2620678.2620683.
• Programming and Reasoning with Algebraic Effects and Dependent Types, Edwin Brady. 2013. In Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming 2013 (ICFP '13). DOI: 10.1145/2500365.2500581.
• Idris — Systems Programming Meets Full Dependent Types, Edwin Brady. 2011. In Proceedings of the 5th ACM workshop on Programming Languages meets Program Verification 2011 (PLPV '11). DOI: 10.1145/1929529.1929536.
• Scrapping your Inefficient Engine: using Partial Evaluation to Improve Domain-Specific Language Implementation, Edwin Brady and Kevin Hammond. 2010. In Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming 2010 (ICFP '10). DOI: 10.1145/1863543.1863587.