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
García-Pérez, Álvaro; Nogueira, Pablo The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: a proof via corresponding calculus. (English) Zbl 1493.68085 J. Funct. Program. 29, Paper No. e7, 38 p. (2019). MSC: 68N18 68Q55 PDFBibTeX XMLCite \textit{Á. García-Pérez} and \textit{P. Nogueira}, J. Funct. Program. 29, Paper No. e7, 38 p. (2019; Zbl 1493.68085) Full Text: DOI