Create Papers page

.github/PULL_REQUEST_TEMPLATE/new_paper.md

@@ -0,0 +1,19 @@
+# Add paper involving Idris
+
+## Title
+
+
+## Authors
+
+
+## Citation Details
+
+<!-- Ideally this should be in ACM or IEEE format -->
+
+## CHECKLIST
+
+- [ ] I have included hyperlinks to the official catalogue.
+- [ ] I have specified the DOI (Digital Object Identifier) of the document.
+- [ ] If there is no Open Access copy, I have included a link to an author's
+    version or a preprint (for example, arXiv).
+

src/content/pages/docs/index.rst

@@ -45,33 +45,3 @@ Additionally, the
 `old Idris 1 Wiki <https://github.com/idris-lang/Idris-dev/wiki>`_
 contains a lot of community supplied information. 
 
-
-Related Publications
---------------------
-
-There are several academic publications associated with Idris, including:
-
-* `Value Dependent Session Design in a Dependently Typed Language <https://www.type-driven.org.uk/edwinb/papers/places2019.pdf>`_, Jan de Muijnck-Hughes, Wim Vanderbauwhede and Edwin Brady,
-  PLACES 2019
-* `Automatically Proving Equivalence by Type-Safe Reflection <https://www.type-driven.org.uk/edwinb/papers/cicm17.pdf>`_, Franck Slama and Edwin Brady,
-  Conference on Intelligent Computer Mathematics (CICM) 2017
-* `Type-driven Development of Concurrent Communicating Systems <https://www.type-driven.org.uk/edwinb/papers/tdd-conc.pdf>`_, Edwin Brady,
-  Computer Science Journal (AGH University of Science and Technology) 2017
-* `Elaboration Reflection: Extending Idris in Idris <https://www.type-driven.org.uk/edwinb/papers/elab-reflection.pdf>`_, David Christiansen and Edwin Brady
-  In proceedings of ICFP 2016
-* `Resource-dependent Algebraic Effects <https://www.type-driven.org.uk/edwinb/papers/dep-eff.pdf>`_, Edwin Brady
-  In proceedings of TFP 2014
-* `Idris, a General Purpose Dependently Typed Programming Language: Design and Implementation <https://www.type-driven.org.uk/edwinb/papers/impldtp.pdf>`_, Edwin Brady
-  In Journal of Functional Programming, October 2013.
-* `Dependent Type Providers <http://www.davidchristiansen.dk/pubs/dependent-type-providers.pdf>`_, David Christiansen
-  In Workshop on Generic Programming, 2013.
-* `Dependent Types for Safe and Secure Web Programming <https://www.type-driven.org.uk/edwinb/papers/ifl2013.pdf>`_, Simon Fowler and Edwin Brady
-  In proceedings of IFL 2013
-* `Programming and Reasoning with Algebraic Effects and Dependent Types <https://www.type-driven.org.uk/edwinb/papers/effects.pdf>`_, Edwin Brady
-  In proceedings of ICFP 2013
-* `Idris – Systems Programming meets Full Dependent Types <https://www.type-driven.org.uk/edwinb/papers/plpv11.pdf>`_, Edwin Brady
-  In proceedings of PLPV 2011.
-* `Scrapping your Inefficient Engine: using Partial Evaluation to Improve Domain-Specific Language Implementation <https://www.type-driven.org.uk/edwinb/papers/icfp10.pdf>`_, Edwin Brady and Kevin Hammond
-  In proceedings of ICFP 2010.
-
-

src/content/pages/papers.rst

@@ -0,0 +1,122 @@
+Papers
+======
+
+The Idris Language
+------------------
+
+* `Idris 2: Quantitative Type Theory in Practice <https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2021.9>`_,
+  Edwin Brady.  2021.  In 35th European Conference on Object-Oriented Programming
+  (ECOOP 2021).
+  DOI: `10.4230/LIPIcs.ECOOP.2021.9 <https://doi.org/10.4230/LIPIcs.ECOOP.2021.9>`_.
+* `Idris, a General Purpose Dependently Typed Programming Language: Design and Implementation <https://www.type-driven.org.uk/edwinb/papers/impldtp.pdf>`_,
+  Edwin Brady.  2013.  In Journal of Functional Programming (JFP).
+  DOI: `10.1017/S095679681300018X <https://doi.org/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 <https://github.com/idris-lang/idris-lang.github.io/pulls>`_.
+
+* `Frex: Dependently Typed Algebraic Simplification <https://dl.acm.org/doi/10.1145/3747506>`_,
+  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 <https://doi.org/10.1145/3747506>`_.
+* `Towards Coherent Semantics: A Quantitatively Typed EDSL for Synchronous System Design <https://ieeexplore.ieee.org/abstract/document/10992876>`_,
+  Rui Chen and Ingo Sander.  2025.  Design, Automation & Test in Europe
+  Conference (DATE).
+  DOI: `10.23919/DATE64628.2025.10992876 <https://doi.org/10.23919/DATE64628.2025.10992876>`_.
+* `Towards being positively negative about dependent types <https://pureportal.strath.ac.uk/en/publications/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 <https://ieeexplore.ieee.org/abstract/document/10673844>`_,
+  Rui Chen and Ingo Sander.  2024.  In Forum on Specification & Design Languages
+  (FDL).
+  DOI: `10.1109/FDL63219.2024.10673844 <https://doi.org/10.1109/FDL63219.2024.10673844>`_.
+* `Type-Level Property Based Testing <https://dl.acm.org/doi/10.1145/3678000.3678206>`_,
+  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 <https://doi.org/10.1145/3678000.3678206>`_.
+* `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->`_,
+  Denis Buzdalov.  2024.  Extended Abstract Presented at the 9th ACM
+  SIGPLAN International Workshop on Type-Driven Development (TyDe 2024).
+* `Colouring flags with Dafny & Idris <https://pureportal.strath.ac.uk/en/publications/colouring-flags-with-dafny-amp-idris>`_,
+  Jan de Muijnck-Hughes and James Noble.  2024.  Paper presented at Dafny 2024.
+* `Wiring Circuits Is Easy as {0,1,ω}, or Is It... <https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2023.8>`_,
+  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 <https://doi.org/10.4230/LIPIcs.ECOOP.2023.8>`_.
+* `Builtin Types Viewed as Inductive Families <https://link.springer.com/chapter/10.1007/978-3-031-30044-8_5>`_,
+  Guillaume Allais.  2023.  In Proceedings of the 32nd European Symposium on
+  Programming (ESOP 2023).
+  DOI: `10.1007/978-3-031-30044-8_5 <https://doi.org/10.1007/978-3-031-30044-8_5>`_.
+* `Type-safe Quantum Programming in Idris <https://link.springer.com/chapter/10.1007/978-3-031-30044-8_19>`_,
+  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 <https://doi.org/10.1007/978-3-031-30044-8_19>`_.
+* `Type Theory as a Language Workbench <https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.EVCS.2023.9>`_,
+  Jan de Muijnck-Hughes, Guillaume Allais, and Edwin Brady.  2023.  In Eelco
+  Visser Commemorative Symposium (EVCS 2023).
+  DOI: `10.4230/OASIcs.EVCS.2023.9 <https://doi.org/10.4230/OASIcs.EVCS.2023.9>`_.
+* `Dependent tagless final <https://dl.acm.org/doi/10.1145/3498886.3502201>`_,
+  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 <https://doi.org/10.1145/3498886.3502201>`_.
+* `A Typing Discipline for Hardware Interfaces <https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.6>`_,
+  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 <https://doi.org/10.4230/LIPIcs.ECOOP.2019.6>`_.
+* `Building a Blockchain Simulation using the Idris Programming Language <https://dl.acm.org/doi/abs/10.1145/3299815.3314456>`_,
+  Qiutai Pan and Xenofon Koutsoukos.  2019.  In Proceedings of the 2019 ACM
+  Southeast Conference (ACMSE '19).
+  DOI: `10.1145/3299815.3314456 <https://doi.org/10.1145/3299815.3314456>`_.
+* `Value Dependent Session Design in a Dependently Typed Language <https://www.type-driven.org.uk/edwinb/papers/places2019.pdf>`_,
+  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 <https://doi.org/10.4204/EPTCS.291.5>`_.
+* `Typing, representing, and abstracting control: functional pearl <https://dl.acm.org/doi/10.1145/3240719.3241788>`_,
+  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 <https://doi.org/10.1145/3240719.3241788>`_.
+* `Automatically Proving Equivalence by Type-Safe Reflection <https://www.type-driven.org.uk/edwinb/papers/cicm17.pdf>`_,
+  Franck Slama and Edwin Brady.  2017.  In Conference on Intelligent Computer
+  Mathematics (CICM) 2017.
+  DOI: `10.1007/978-3-319-62075-6_4 <https://doi.org/10.1007/978-3-319-62075-6_4>`_.
+* `Type-driven Development of Concurrent Communicating Systems <https://www.type-driven.org.uk/edwinb/papers/tdd-conc.pdf>`_,
+  Edwin Brady.  2017.  Computer Science Journal (CSCI).  AGH University of Science and
+  Technology.
+  DOI: `10.7494/csci.2017.18.3.1413 <https://doi.org/10.7494/csci.2017.18.3.1413>`_.
+* `Elaboration Reflection: Extending Idris in Idris <https://www.type-driven.org.uk/edwinb/papers/elab-reflection.pdf>`_,
+  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 <https://doi.org/10.1145/2951913.2951932>`_.
+* `Resource-dependent Algebraic Effects <https://www.type-driven.org.uk/edwinb/papers/dep-eff.pdf>`_,
+  Edwin Brady.  2014.  In Proceedings of Trends in Functional Programming (TFP).
+  DOI: `10.1007/978-3-319-14675-1_2 <https://doi.org/10.1007/978-3-319-14675-1_2>`_.
+* `Dependent Type Providers <http://www.davidchristiansen.dk/pubs/dependent-type-providers.pdf>`_,
+  David Christiansen.  2013.  In Proceedings of the 9th ACM SIGPLAN workshop on
+  Generic Programming (WGP '13).
+  DOI: `10.1145/2502488.2502495 <https://doi.org/10.1145/2502488.2502495>`_.
+* `Dependent Types for Safe and Secure Web Programming <https://www.type-driven.org.uk/edwinb/papers/ifl2013.pdf>`_,
+  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 <https://doi.org/10.1145/2620678.2620683>`_.
+* `Programming and Reasoning with Algebraic Effects and Dependent Types <https://www.type-driven.org.uk/edwinb/papers/effects.pdf>`_,
+  Edwin Brady.  2013.  In Proceedings of the 18th ACM SIGPLAN International
+  Conference on Functional Programming 2013 (ICFP '13).
+  DOI: `10.1145/2500365.2500581 <https://doi.org/10.1145/2500365.2500581>`_.
+* `Idris — Systems Programming Meets Full Dependent Types <https://www.type-driven.org.uk/edwinb/papers/plpv11.pdf>`_,
+  Edwin Brady.  2011.  In Proceedings of the 5th ACM workshop on Programming
+  Languages meets Program Verification 2011 (PLPV '11).
+  DOI: `10.1145/1929529.1929536 <https://doi.org/10.1145/1929529.1929536>`_.
+* `Scrapping your Inefficient Engine: using Partial Evaluation to Improve Domain-Specific Language Implementation <https://www.type-driven.org.uk/edwinb/papers/icfp10.pdf>`_,
+  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 <https://doi.org/10.1145/1863543.1863587>`_.