CPS translations and applications: The cube and beyond
From MaRDI portal
Publication:1125574
DOI10.1023/A:1010000206149zbMath0936.03015OpenAlexW1580682610MaRDI QIDQ1125574
John Hatcliff, Morten Heine B. Sørensen, Gilles Barthe
Publication date: 30 January 2000
Published in: Higher-Order and Symbolic Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1023/a:1010000206149
calculus of constructionslambda calculusdependent typeslogical frameworkscontinuation passing style translations of typed \(\lambda\)-calculidirect style translationsdomain-free \(\lambda\)-cubedomain-free pure type systems
Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Combinatory logic and lambda calculus (03B40)
Related Items
ANF preserves dependent types up to extensional equality ⋮ A Classical Sequent Calculus with Dependent Types ⋮ Unnamed Item ⋮ The undecidability of type related problems in the type-free style System F with finitely stratified polymorphic types ⋮ On one-pass CPS transformations ⋮ Weak normalization implies strong normalization in a class of non-dependent pure type systems ⋮ An induction principle for pure type systems ⋮ CPS-translation as adjoint
Uses Software