CPS translations and applications: The cube and beyond

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

zbMATH Keywords

calculus of constructionslambda calculusdependent typeslogical frameworkscontinuation passing style translations of typed \(\lambda\)-calculidirect style translationsdomain-free \(\lambda\)-cubedomain-free pure type systems

Mathematics Subject Classification ID

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

• Automath