Skip to content

Commit d9c64cd

Browse files
committed
[ papers ] Add numerous papers involving Idris
Put together from a combination of Google Scholar, andrevidela/idris-documentation-tracking#7, Pure portals, and https://github.com/gallais/great-library-of-idris. If I missed anyone, I'm very sorry!
1 parent 23c7c8b commit d9c64cd

File tree

1 file changed

+61
-1
lines changed

1 file changed

+61
-1
lines changed

src/content/pages/papers.rst

Lines changed: 61 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,16 +12,76 @@ The Idris Language
1212
Edwin Brady. 2013. In Journal of Functional Programming (JFP).
1313
DOI: `10.1017/S095679681300018X <https://doi.org/10.1017/S095679681300018X>`_.
1414

15+
1516
Associated Publications
1617
-----------------------
1718

18-
There are several academic publications associated with Idris, including:
19+
There are numerous academic publications associated with Idris, including:
1920

21+
* `Frex: Dependently Typed Algebraic Simplification <https://dl.acm.org/doi/10.1145/3747506>`_,
22+
Guillaume Allais, Edwin Brady, Nathan Corbyn, Ohad Kammar, and Jeremy Yallop.
23+
2025. Proceedings of the ACM on Programming Languages, Volume 9, Issue
24+
International Conference on Functional Programming (ICFP)
25+
(August 2025).
26+
DOI: `10.1145/3747506 <https://doi.org/10.1145/3747506>`_.
27+
* `Towards Coherent Semantics: A Quantitatively Typed EDSL for Synchronous System Design <https://ieeexplore.ieee.org/abstract/document/10992876>`_,
28+
Rui Chen and Ingo Sander. 2025. Design, Automation & Test in Europe
29+
Conference (DATE).
30+
DOI: `10.23919/DATE64628.2025.10992876 <https://doi.org/10.23919/DATE64628.2025.10992876>`_.
31+
* `Towards being positively negative about dependent types <https://pureportal.strath.ac.uk/en/publications/towards-being-positively-negative-about-dependent-types>`_,
32+
Jan de Muijnck-Hughes. 2025. Extended Abstract Presented at the 31st
33+
Conference on Types for Proofs and Programs.
34+
* `A Quantitative Type Approach to Formal Component-Based System Design <https://ieeexplore.ieee.org/abstract/document/10673844>`_,
35+
Rui Chen and Ingo Sander. 2024. In Forum on Specification & Design Languages
36+
(FDL).
37+
DOI: `10.1109/FDL63219.2024.10673844 <https://doi.org/10.1109/FDL63219.2024.10673844>`_.
38+
* `Type-Level Property Based Testing <https://dl.acm.org/doi/10.1145/3678000.3678206>`_,
39+
Thomas Ekström Hansen and Edwin Brady. 2024. In Proceedings of the 9th ACM
40+
SIGPLAN International Workshop on Type-Driven Development (TyDe 2024).
41+
DOI: `10.1145/3678000.3678206 <https://doi.org/10.1145/3678000.3678206>`_.
42+
* `Dependent Types to Push Corners of the Property-based Testing <https://icfp24.sigplan.org/details/tyde-2024-papers/6/Dependent-Types-to-Push-Corners-of-the-Property-based-Testing-Extended-Abstract->`_,
43+
Denis Buzdalov. 2024. Extended Abstract Presented at the 9th ACM
44+
SIGPLAN International Workshop on Type-Driven Development (TyDe 2024).
45+
* `Colouring flags with Dafny & Idris <https://pureportal.strath.ac.uk/en/publications/colouring-flags-with-dafny-amp-idris>`_,
46+
Jan de Muijnck-Hughes and James Noble. 2024. Paper presented at Dafny 2024.
47+
* `Wiring Circuits Is Easy as {0,1,ω}, or Is It... <https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2023.8>`_,
48+
Jan de Muijnck-Hughes and Wim Vanderbauwhede. 2023. In 37th European
49+
Conference on Object-Oriented Programming (ECOOP 2023).
50+
DOI: `10.4230/LIPIcs.ECOOP.2023.8 <https://doi.org/10.4230/LIPIcs.ECOOP.2023.8>`_.
51+
* `Builtin Types Viewed as Inductive Families <https://link.springer.com/chapter/10.1007/978-3-031-30044-8_5>`_,
52+
Guillaume Allais. 2023. In Proceedings of the 32nd European Symposium on
53+
Programming (ESOP 2023).
54+
DOI: `10.1007/978-3-031-30044-8_5 <https://doi.org/10.1007/978-3-031-30044-8_5>`_.
55+
* `Type-safe Quantum Programming in Idris <https://link.springer.com/chapter/10.1007/978-3-031-30044-8_19>`_,
56+
Liliane-Joy Dandy, Emmanuel Jeandel, and Vladimir Zamdzhiev. 2023. In
57+
Proceedings of the 32nd European Symposium on Programming (ESOP 2023).
58+
DOI: `10.1007/978-3-031-30044-8_19 <https://doi.org/10.1007/978-3-031-30044-8_19>`_.
59+
* `Type Theory as a Language Workbench <https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.EVCS.2023.9>`_,
60+
Jan de Muijnck-Hughes, Guillaume Allais, and Edwin Brady. 2023. In Eelco
61+
Visser Commemorative Symposium (EVCS 2023).
62+
DOI: `10.4230/OASIcs.EVCS.2023.9 <https://doi.org/10.4230/OASIcs.EVCS.2023.9>`_.
63+
* `Dependent tagless final <https://dl.acm.org/doi/10.1145/3498886.3502201>`_,
64+
Nicolas Biri. 2022. In Proceedings of the 2022 ACM SIGPLAN International
65+
Workshop on Partial Evaluation and Program Manipulation (PEPM 2022).
66+
DOI: `10.1145/3498886.3502201 <https://doi.org/10.1145/3498886.3502201>`_.
67+
* `A Typing Discipline for Hardware Interfaces <https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.6>`_,
68+
Jan de Muijnck-Hughes and Wim Vanderbauwhede. 2019. In 33rd European
69+
Conference on Object-Oriented Programming (ECOOP 2019).
70+
DOI: `10.4230/LIPIcs.ECOOP.2019.6 <https://doi.org/10.4230/LIPIcs.ECOOP.2019.6>`_.
71+
* `Building a Blockchain Simulation using the Idris Programming Language <https://dl.acm.org/doi/abs/10.1145/3299815.3314456>`_,
72+
Qiutai Pan and Xenofon Koutsoukos. 2019. In Proceedings of the 2019 ACM
73+
Southeast Conference (ACMSE '19).
74+
DOI: `10.1145/3299815.3314456 <https://doi.org/10.1145/3299815.3314456>`_.
2075
* `Value Dependent Session Design in a Dependently Typed Language <https://www.type-driven.org.uk/edwinb/papers/places2019.pdf>`_,
2176
Jan de Muijnck-Hughes, Wim Vanderbauwhede, and Edwin Brady. 2019. In
2277
Proceedings of Programming Language Approaches to Concurrency- and
2378
Communication-cEntric Software (PLACES) 2019.
2479
DOI: `10.4204/EPTCS.291.5 <https://doi.org/10.4204/EPTCS.291.5>`_.
80+
* `Typing, representing, and abstracting control: functional pearl <https://dl.acm.org/doi/10.1145/3240719.3241788>`_,
81+
Philipp Schuster and Jonathan Immanuel Brachthäuser. 2018. In Proceedings of
82+
the 3rd ACM SIGPLAN International Workshop on Type-Driven Development (TyDe
83+
2018).
84+
doi: `10.1145/3240719.3241788 <https://doi.org/10.1145/3240719.3241788>`_.
2585
* `Automatically Proving Equivalence by Type-Safe Reflection <https://www.type-driven.org.uk/edwinb/papers/cicm17.pdf>`_,
2686
Franck Slama and Edwin Brady. 2017. In Conference on Intelligent Computer
2787
Mathematics (CICM) 2017.

0 commit comments

Comments
 (0)