Affeldt, Reynald; Garrigue, Jacques; Nowak, David; Saikawa, Takafumi A trustful monad for axiomatic reasoning with probability and nondeterminism. (English) Zbl 1493.03004 J. Funct. Program. 31, Paper No. e17, 38 p. (2021). Reviewer: Alexandre Goy (Lyon) MSC: 03B70 03B35 68N18 68V15 PDFBibTeX XMLCite \textit{R. Affeldt} et al., J. Funct. Program. 31, Paper No. e17, 38 p. (2021; Zbl 1493.03004) Full Text: DOI arXiv
Convent, Lukas; Lindley, Sam; McBride, Conor; McLaughlin, Craig Doo bee doo bee doo. (English) Zbl 1442.68026 J. Funct. Program. 30, Paper No. e9, 53 p. (2020). MSC: 68N18 68N15 PDFBibTeX XMLCite \textit{L. Convent} et al., J. Funct. Program. 30, Paper No. e9, 53 p. (2020; Zbl 1442.68026) Full Text: DOI
Cockx, Jesper; Abel, Andreas Elaborating dependent (co)pattern matching: no pattern left behind. (English) Zbl 1442.68025 J. Funct. Program. 30, Paper No. e2, 43 p. (2020). MSC: 68N18 68N15 PDFBibTeX XMLCite \textit{J. Cockx} and \textit{A. Abel}, J. Funct. Program. 30, Paper No. e2, 43 p. (2020; Zbl 1442.68025) Full Text: DOI
Farka, František; Komendantskya, Ekaterina; Hammond, Kevin Proof-relevant Horn clauses for dependent type inference and term synthesis. (English) Zbl 1451.68323 Theory Pract. Log. Program. 18, No. 3-4, 484-501 (2018). MSC: 68V15 03B35 68N17 68N18 PDFBibTeX XMLCite \textit{F. Farka} et al., Theory Pract. Log. Program. 18, No. 3--4, 484--501 (2018; Zbl 1451.68323) Full Text: DOI arXiv
Botta, Nicola; Jansson, Patrik; Ionescu, Cezar Contributions to a computational theory of policy advice and avoidability. (English) Zbl 1476.68049 J. Funct. Program. 27, Paper No. e23, 52 p. (2017). MSC: 68N18 03B70 91B06 PDFBibTeX XMLCite \textit{N. Botta} et al., J. Funct. Program. 27, Paper No. e23, 52 p. (2017; Zbl 1476.68049) Full Text: DOI
Dagand, Pierre-Evariste The essence of ornaments. (English) Zbl 1418.68032 J. Funct. Program. 27, Paper No. e9, 27 p. (2017). MSC: 68N18 68N30 68Q65 PDFBibTeX XMLCite \textit{P.-E. Dagand}, J. Funct. Program. 27, Paper No. e9, 27 p. (2017; Zbl 1418.68032) Full Text: DOI
Cockx, Jesper; Devriese, Dominique; Piessens, Frank Eliminating dependent pattern matching without K. (English) Zbl 1419.68037 J. Funct. Program. 26, Paper No. e16, 40 p. (2016). MSC: 68N18 03B15 03G30 55U40 PDFBibTeX XMLCite \textit{J. Cockx} et al., J. Funct. Program. 26, Paper No. e16, 40 p. (2016; Zbl 1419.68037) Full Text: DOI
Yang, Yanpeng; Bi, Xuan; Oliveira, Bruno C. d. S. Unified syntax with iso-types. (English) Zbl 1483.68065 Igarashi, Atsushi (ed.), Programming languages and systems. 14th Asian symposium, APLAS 2016, Hanoi, Vietnam, November 21–23, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10017, 251-270 (2016). MSC: 68N18 68N15 PDFBibTeX XMLCite \textit{Y. Yang} et al., Lect. Notes Comput. Sci. 10017, 251--270 (2016; Zbl 1483.68065) Full Text: DOI
McBride, Conor I got plenty o’ nuttin’. (English) Zbl 1343.68060 Lindley, Sam (ed.) et al., A list of successes that can change the world. Essays dedicated to Philip Wadler on the occasion of his 60th birthday. Cham: Springer (ISBN 978-3-319-30935-4/pbk; 978-3-319-30936-1/ebook). Lecture Notes in Computer Science 9600, 207-233 (2016). MSC: 68N30 03B70 03F52 68N18 PDFBibTeX XMLCite \textit{C. McBride}, Lect. Notes Comput. Sci. 9600, 207--233 (2016; Zbl 1343.68060) Full Text: DOI
Bizjak, Aleš; Grathwohl, Hans Bugge; Clouston, Ranald; Møgelberg, Rasmus E.; Birkedal, Lars Guarded dependent type theory with coinductive types. (English) Zbl 1475.68060 Jacobs, Bart (ed.) et al., Foundations of software science and computation structures. 19th international conference, FOSSACS 2016, held as part of the European joint conferences on theory and practice of software, ETAPS 2016, Eindhoven, The Netherlands, April 2–8, 2016. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 9634, 20-35 (2016). MSC: 68N18 03B38 03B70 68N30 PDFBibTeX XMLCite \textit{A. Bizjak} et al., Lect. Notes Comput. Sci. 9634, 20--35 (2016; Zbl 1475.68060) Full Text: DOI arXiv
Eisenberg, Richard A.; Weirich, Stephanie; Ahmed, Hamidhasan G. Visible type application. (English) Zbl 1335.68031 Thiemann, Peter (ed.), Programming languages and systems. 25th European symposium on programming, ESOP 2016, held as part of the European joint conferences on theory and practice of software, ETAPS 2016, Eindhoven, The Netherlands, April 2–8, 2016. Proceedings. Berlin: Springer (ISBN 978-3-662-49497-4/pbk; 978-3-662-49498-1/ebook). Lecture Notes in Computer Science 9632, 229-254 (2016). MSC: 68N18 PDFBibTeX XMLCite \textit{R. A. Eisenberg} et al., Lect. Notes Comput. Sci. 9632, 229--254 (2016; Zbl 1335.68031) Full Text: DOI Link
Casinghino, Chris; Sjöberg, Vilhelm; Weirich, Stephanie Combining proofs and programs in a dependently typed language. (English) Zbl 1284.68125 Proceedings of the 41st ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’14, San Diego, CA, USA, January 22–24, 2014. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-2544-8). 33-45 (2014). MSC: 68N18 68Q60 68N30 68Q55 03B40 03B70 PDFBibTeX XMLCite \textit{C. Casinghino} et al., in: Proceedings of the 41st ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL '14, San Diego, CA, USA, January 22--24, 2014. New York, NY: Association for Computing Machinery (ACM). 33--45 (2014; Zbl 1284.68125) Full Text: DOI Link
Brady, Edwin Idris, a general-purpose dependently typed programming language: design and implementation. (English) Zbl 1295.68059 J. Funct. Program. 23, No. 5, 552-593 (2013). Reviewer: Valentina Dagienë (Vilnius) MSC: 68N18 68N15 PDFBibTeX XMLCite \textit{E. Brady}, J. Funct. Program. 23, No. 5, 552--593 (2013; Zbl 1295.68059) Full Text: DOI