@@ -37,28 +37,26 @@ dependent types in general, can be obtained from various sources:
3737
3838 * https://github.com/idris-community
3939
40- * Various papers (e.g. [#BradyHammond2012 ]_, [#Brady ]_, and [#BradyHammond2010 ]_). Although these mostly
41- describe older versions of Idris.
42-
43- .. [#BradyHammond2012 ] Edwin Brady and Kevin Hammond. 2012. Resource-Safe systems
44- programming with embedded domain specific languages. In
45- Proceedings of the 14th international conference on Practical
46- Aspects of Declarative Languages (PADL'12), Claudio Russo and
47- Neng-Fa Zhou (Eds.). Springer-Verlag, Berlin, Heidelberg,
48- 242-257. DOI=10.1007/978-3-642-27694-1_18
49- https://dx.doi.org/10.1007/978-3-642-27694-1_18
50-
51- .. [#Brady ] Edwin C. Brady. 2011. IDRIS ---: systems programming meets full
40+ * The papers describing Idris2 [#Brady2021 ]_ and the older Idris1
41+ [#Brady2011 ]_ [#Brady2013 ]_. There is a wider (non-exhaustive) list of
42+ papers involving Idris
43+ `on the website <https://www.idris-lang.org/pages/papers.html >`_.
44+
45+
46+ .. [#Brady2021 ] Edwin Brady. Idris 2: Quantitative Type Theory in Practice. In
47+ 35th European Conference on Object-Oriented Programming (ECOOP 2021).
48+ Leibniz International Proceedings in Informatics (LIPIcs), Volume 194,
49+ pp. 9:1-9:26, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)
50+ https://doi.org/10.4230/LIPIcs.ECOOP.2021.9
51+
52+ .. [#Brady2013 ] E. BRADY, "Idris, a general-purpose dependently typed
53+ programming language: Design and implementation," Journal of Functional
54+ Programming, vol. 23, no. 5, pp. 552-593, 2013.
55+ doi:10.1017/S095679681300018X https://doi.org/10.1017/S095679681300018X
56+
57+ .. [#Brady2011 ] Edwin C. Brady. 2011. IDRIS ---: systems programming meets full
5258 dependent types. In Proceedings of the 5th ACM workshop on
5359 Programming languages meets program verification (PLPV
5460 '11). ACM, New York, NY, USA,
5561 43-54. DOI=10.1145/1929529.1929536
5662 https://doi.acm.org/10.1145/1929529.1929536
57-
58- .. [#BradyHammond2010 ] Edwin C. Brady and Kevin Hammond. 2010. Scrapping your
59- inefficient engine: using partial evaluation to improve
60- domain-specific language implementation. In Proceedings of the
61- 15th ACM SIGPLAN international conference on Functional
62- programming (ICFP '10). ACM, New York, NY, USA,
63- 297-308. DOI=10.1145/1863543.1863587
64- https://doi.acm.org/10.1145/1863543.1863587
0 commit comments