Annenkov, Danil; Milo, Mikkel; Nielsen, Jakob Botsch; Spitters, Bas Extracting functional programs from Coq, in Coq. (English) Zbl 07581654 J. Funct. Program. 32, Paper No. e11, 60 p. (2022). MSC: 68N18 PDFBibTeX XMLCite \textit{D. Annenkov} et al., J. Funct. Program. 32, Paper No. e11, 60 p. (2022; Zbl 07581654) Full Text: DOI arXiv
Huang, Xuejing; Zhao, Jinxu; Oliveira, Bruno C. d. S. Taming the merge operator. (English) Zbl 1519.68049 J. Funct. Program. 31, Paper No. e28, 67 p. (2021). MSC: 68N18 03B70 68V20 PDFBibTeX XMLCite \textit{X. Huang} et al., J. Funct. Program. 31, Paper No. e28, 67 p. (2021; Zbl 1519.68049) Full Text: DOI
Accattoli, Beniamino; Graham-Lengrand, Stéphane; Kesner, Delia Tight typings and split bounds, fully developed. (English) Zbl 1482.68077 J. Funct. Program. 30, Paper No. e14, 101 p. (2020). MSC: 68N18 68N30 PDFBibTeX XMLCite \textit{B. Accattoli} et al., J. Funct. Program. 30, Paper No. e14, 101 p. (2020; Zbl 1482.68077) Full Text: DOI arXiv
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
Hamana, Makoto How to prove decidability of equational theories with second-order computation analyser SOL. (English) Zbl 1442.68027 J. Funct. Program. 29, Paper No. e20, 53 p. (2019). MSC: 68N18 03B25 03B40 03B70 18M05 68N15 68N30 68V15 PDFBibTeX XMLCite \textit{M. Hamana}, J. Funct. Program. 29, Paper No. e20, 53 p. (2019; Zbl 1442.68027) Full Text: DOI
Schrijvers, Tom; Oliveira, Bruno C. d. S.; Wadler, Philip; Marntirosian, Koar COCHIS: stable and coherent implicits. (English) Zbl 1493.68094 J. Funct. Program. 29, Paper No. e3, 82 p. (2019). MSC: 68N18 03B70 PDFBibTeX XMLCite \textit{T. Schrijvers} et al., J. Funct. Program. 29, Paper No. e3, 82 p. (2019; Zbl 1493.68094) Full Text: DOI
Blanqui, Frédéric Size-based termination of higher-order rewriting. (English) Zbl 1476.68048 J. Funct. Program. 28, Paper No. e11, 75 p. (2018). MSC: 68N18 68Q42 PDFBibTeX XMLCite \textit{F. Blanqui}, J. Funct. Program. 28, Paper No. e11, 75 p. (2018; Zbl 1476.68048) Full Text: DOI arXiv
Dagand, Pierre-Évariste; Tabareau, Nicolas; Tanter, Éric Foundations of dependent interoperability. (English) Zbl 1476.68051 J. Funct. Program. 28, Paper No. e9, 44 p. (2018). MSC: 68N18 68N30 68Q55 PDFBibTeX XMLCite \textit{P.-É. Dagand} et al., J. Funct. Program. 28, Paper No. e9, 44 p. (2018; Zbl 1476.68051) Full Text: DOI
Ziliani, Beta; Sozeau, Matthieu A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading. (English) Zbl 1418.68185 J. Funct. Program. 27, Paper No. e10, 63 p. (2017). MSC: 68T15 PDFBibTeX XMLCite \textit{B. Ziliani} and \textit{M. Sozeau}, J. Funct. Program. 27, Paper No. e10, 63 p. (2017; Zbl 1418.68185) Full Text: DOI
Lakin, Matthew R.; Pitts, Andrew M. Contextual equivalence for inductive definitions with binders in higher order typed functional programming. (English) Zbl 1300.68017 J. Funct. Program. 23, No. 6, 658-700 (2013). MSC: 68N18 PDFBibTeX XMLCite \textit{M. R. Lakin} and \textit{A. M. Pitts}, J. Funct. Program. 23, No. 6, 658--700 (2013; Zbl 1300.68017) Full Text: DOI
Pientka, Brigitte An insider’s look at LF type reconstruction: everything you (n)ever wanted to know. (English) Zbl 1262.68030 J. Funct. Program. 23, No. 1, 1-37 (2013). MSC: 68N18 68N15 68N30 03B70 PDFBibTeX XMLCite \textit{B. Pientka}, J. Funct. Program. 23, No. 1, 1--37 (2013; Zbl 1262.68030) Full Text: DOI
Park, Sungwoo; Im, Hyeonseung Type-safe higher-order channels with channel locality. (English) Zbl 1162.68394 J. Funct. Program. 19, No. 1, 107-142 (2009). MSC: 68N18 PDFBibTeX XMLCite \textit{S. Park} and \textit{H. Im}, J. Funct. Program. 19, No. 1, 107--142 (2009; Zbl 1162.68394) Full Text: DOI
Burn, Geoffrey; Le Métayer, Daniel Proving the correctness of compiler optimisations based on a global analysis: A study of strictness analysis. (English) Zbl 0854.68018 J. Funct. Program. 6, No. 1, 75-109 (1996). MSC: 68N20 PDFBibTeX XMLCite \textit{G. Burn} and \textit{D. Le Métayer}, J. Funct. Program. 6, No. 1, 75--109 (1996; Zbl 0854.68018) Full Text: DOI
Consel, Charles; Khoo, Siau Cheng On-line and off-line partial evaluation: Semantic specifications and correctness proofs. (English) Zbl 0846.68062 J. Funct. Program. 5, No. 4, 461-500 (1995). MSC: 68Q55 68Q60 PDFBibTeX XMLCite \textit{C. Consel} and \textit{S. C. Khoo}, J. Funct. Program. 5, No. 4, 461--500 (1995; Zbl 0846.68062) Full Text: DOI