An equivalence-preserving CPS translation via multi-language semantics

No abstract is available for this paper.

• Publication year

  2011

• Venue

  ACM SIGPLAN International Conference on Functional Programming

• Publication date

  2011-09-19

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1145/2034773.2034830
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Linear and Affine Typing of Continuation-Passing Style

  2013cited by this paper
• An Equivalence-Preserving CPS Translation via Multi-Language Semantics ( Technical Appendix )

  2012influential reference
• Realizability and Compositional Compiler Correctness for a Polymorphic Language

  2010cited by this paper
• Biorthogonality, step-indexing and compiler correctness

  2009cited by this paper
• State-dependent representation independence

  2009cited by this paper
• Typed closure conversion preserves observational equivalence

  2008influential reference
• Abstract Predicates and Mutable ADTs in Hoare Type Theory

  2007cited by this paper
• Fully abstract semantics of additive aspects by translation

  2007cited by this paper
• Operational semantics for multi-language programs

  2007cited by this paper
• A certified type-preserving compiler from lambda calculus to assembly language

  2007cited by this paper
• Compiling with continuations, continued

  2007cited by this paper
• Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types

  2006cited by this paper
• Securing the .NET programming model

  2006cited by this paper
• Proving Noninterference by a Fully Complete Translation to the Simply Typed Lambda-Calculus

  2006cited by this paper
• Genericity and the π-calculus

  2005cited by this paper
• Game semantics and linear CPS interpretation

  2005influential reference
• Answer Type Polymorphism in Call-by-Name Continuation Passing

  2004cited by this paper
• From control effects to typed continuation passing

  2003cited by this paper
• Linear Continuation-Passing

  2002cited by this paper
• Extracting the Range of cps from Affine Typing

  2002influential reference
• A uniform type structure for secure information flow

  2002cited by this paper
• Linearly Used Effects: Monadic and CPS Transformations into the Linear Lambda Calculus

  2002cited by this paper
• Sequentiality and the π-Calculus

  2001influential reference
• Secure Information Flow and CPS

  2001influential reference
• Sequentiality and the pi-Calculus

  2001cited by this paper
• On Full Abstraction for PCF: I, II, and III

  2000cited by this paper
• From system F to typed assembly language

  1999influential reference
• Protection in Programming-Language Translations

  1998cited by this paper
• Isolating side effects in sequential languages

  1995influential reference
• A type-based compiler for standard ML

  1995cited by this paper
• A fully abstract semantics for a concurrent functional language with monadic types

  1995cited by this paper
• Full Abstraction for PCF

  1994cited by this paper
• Representing monads

  1994influential reference
• Explicit polymorphism and CPS conversion

  1993cited by this paper
• Back to Direct Style

  1992influential reference
• Observable sequentiality and full abstraction

  1992cited by this paper
• Reasoning about programs in continuation-passing style

  1992cited by this paper
• Fully abstract translations between functional languages

  1991influential reference
• Equivalence in functional languages with effects

  1991cited by this paper
• Compiling with Continuations

  1991cited by this paper
• Theorems for free!

  1989influential reference
• Continuations may be unreasonable

  1988influential reference
• Towards fully abstract semantics for local variables

  1988cited by this paper
• Orbit: an optimizing compiler for scheme

  1988cited by this paper
• Orbit: an optimizing compiler for scheme

  1986cited by this paper
• Continuation Semantics in Typed Lambda-Calculi (Summary)

  1985cited by this paper
• Types, Abstraction and Parametric Polymorphism

  1983cited by this paper
• Rabbit: A Compiler for Scheme

  1978cited by this paper
• Fully Abstract Models of Typed lambda-Calculi

  1977cited by this paper
• LCF Considered as a Programming Language

  1977influential reference

• Endangered by the Language But Saved by the Compiler: Robust Safety via Semantic Back-Translation

  2026cites this paper
• SoK: Robust properties, robust abstractions and back-translations

  2026cites this paper
• Pyrosome: Verified Compilation for Modular Metatheory

  2025cites this paper
• A Survey of Multilanguage Interoperability and Its Program Analysis

  2025cites this paper
• Symbolic Parallel Composition for Multi-language Protocol Verification

  2025cites this paper
• The Ethical Compiler: Addressing the Is-Ought Gap in Compilation (Invited Talk)

  2025cites this paper
• Compilation as Multi-Language Semantics

  2025cites this paper
• SECOMP: Formally Secure Compilation of Compartmentalized C Programs

  2024cites this paper
• Learning to Design Novel Programming Languages using CodeBlock Syntax Checker

  2024cites this paper
• On the Operational Theory of the CPS-Calculus: Towards a Theoretical Foundation for IRs

  2024cites this paper
• Semantic Encapsulation using Linking Types

  2023cites this paper
• On multi-language abstraction: Towards a static analysis of multi-language programs

  2023cites this paper
• Secure Composition of Robust and Optimising Compilers

  2023cites this paper
• DimSum: A Decentralized Approach to Multi-language Semantics and Verification

  2023cites this paper
• Two Parametricities Versus Three Universal Types

  2022cites this paper
• Semantic soundness for language interoperability

  2022cites this paper
• ANF preserves dependent types up to extensional equality

  2022cites this paper
• Securing Interruptible Enclaved Execution on Small Microprocessors

  2021cites this paper
• Robustly Safe Compilation, an Efficient Form of Secure Compilation

  2021influential citation
• When Good Components Go Bad: Formally Secure When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise Compilation Despite Dynamic Compromise

  2021cites this paper
• Compiling with continuations, correctly

  2021cites this paper
• SecurePtrs: Proving Secure Compilation with Data-Flow Back-Translation and Turn-Taking Simulation

  2021cites this paper
• CPS transformation with affine types for call-by-value implicit polymorphism

  2021cites this paper
• CapablePtrs: Securely Compiling Partial Programs Using the Pointers-as-Capabilities Principle

  2020cites this paper
• On the Semantic Expressiveness of Iso- and Equi-Recursive Types

  2020cites this paper
• Fully Abstract and Robust Compilation and How to Reconcile the Two, Abstractly

  2020cites this paper
• Equational Logic and Set-Theoretic Models for Multi-Languages

  2020cites this paper
• On the semantic expressiveness of recursive types

  2020influential citation
• Computation focusing

  2020cites this paper
• Equational Logic and Categorical Semantics for Multi-Languages

  2020cites this paper
• Type-directed scheduling of streaming accelerators

  2020cites this paper
• A categorical approach to secure compilation

  2020cites this paper
• Provably Secure Isolation for Interruptible Enclaved Execution on Small Microprocessors

  2020cites this paper
• Symbolic Disintegration with a Variety of Base Measures

  2020cites this paper
• On the Multi-Language Construction

  2019influential citation
• StkTokens: enforcing well-bracketed control flow and stack encapsulation using linear capabilities

  2019cites this paper
• A Brief Tour of Formally Secure Compilation

  2019cites this paper
• The Quest for Formally Secure Compartmentalizing Compilation

  2019influential citation
• Robustly Safe Compilation

  2019influential citation
• Programming Languages and Systems

  2019influential citation
• THE VERIFIERS ? “ Can you trust your compiler ? ” So began

  2019cites this paper
• The next 700 compiler correctness theorems (functional pearl)

  2019cites this paper
• The Next 700 Compiler Correctness Theorems (Functional Pearl)

  2019cites this paper
• Under Control: Compositionally Correct Closure Conversion with Mutable State

  2019cites this paper
• Formal Approaches to Secure Compilation

  2019influential citation
• Reasonably Mixing a Functional Language with Assembly ∗

  2018cites this paper
• 1 Formal Approaches to Secure Compilation

  2018influential citation
• Exploring Robust Property Preservation for Secure Compilation

  2018cites this paper
• When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise

  2018cites this paper
• Journey Beyond Full Abstraction: Exploring Robust Property Preservation for Secure Compilation

  2018influential citation
• Handling delimited continuations with dependent types

  2018cites this paper
• Typed closure conversion for the calculus of constructions

  2018cites this paper
• Robustly Safe Compilation or, Efficient, Provably Secure Compilation

  2018influential citation
• Secure Compilation and Hyperproperty Preservation

  2017influential citation
• Towards Automatic Compartmentalization of C Programs on Capability Machines

  2017cites this paper
• 2nd Summit on Advances in Programming Languages, SNAPL 2017, Asilomar, CA, USA, May 7-10, 2017

  2017cites this paper
• Formally Secure Compilation Last updated : September 1 , 2017 General Information

  2017cites this paper
• Linking Types for Multi-Language Software: Have Your Cake and Eat It Too

  2017cites this paper
• FunTAL: reasonably mixing a functional language with assembly

  2017cites this paper
• Formally Secure Compilation Last updated : January 3 , 2017 General Information

  2017cites this paper
• FabULous Interoperability for ML and a Linear Language

  2017cites this paper
• Type-preserving CPS translation of Σ and Π types is not not possible

  2017cites this paper
• Modular, Fully-abstract Compilation by Approximate Back-translation

  2017cites this paper
• Fully abstract compilation via universal embedding

  2016influential citation
• Supplement to : The key to blame : Gradual typing meets cryptography

  2016cites this paper
• Beyond Good and Evil: Formalizing the Security Guarantees of Compartmentalizing Compilation

  2016cites this paper
• Protecting Functional Programs From Low-Level Attackers

  2016cites this paper
• Security Guarantees for the Execution Infrastructure of Software Applications

  2016cites this paper
• On Modular and Fully-Abstract Compilation

  2016influential citation
• On Modular and Fully-Abstract Compilation - Technical Appendix

  2016influential citation
• Beyond Full Abstraction: Formalizing the Security Guarantees of Low-Level Compartmentalization

  2016cites this paper
• Secure Compilation as Hyperproperties Preservation

  2016influential citation
• Beyond Good and Evil: Formalizing the Security Guarantees of Low-Level Compartmentalization

  2016cites this paper
• Observational program calculi and the correctness of translations

  2015cites this paper
• Secure Compilation to Protected Module Architectures

  2015cites this paper
• Verified Compilers for a Multi-Language World

  2015cites this paper
• Fully-abstract compilation by approximate back-translation

  2015cites this paper
• Noninterference for free

  2015influential citation
• Compositional CompCert

  2015cites this paper
• The Tome of Secure Compilation: Fully Abstract Compilation to Protected Modules Architectures ; Het boek van veilige compilatie: Volledig abstracte compilatie naar beschermende modulearchitecturen

  2015cites this paper
• Fully abstract trace semantics for protected module architectures

  2015cites this paper
• Correct-by-Construction Program Derivation from Specifications to Assembly Language

  2014cites this paper
• Verifying an Open Compiler Using Multi-language Semantics

  2014cites this paper
• Compiler verification meets cross-language linking via data abstraction

  2014cites this paper
• Secure Compilation of Object-Oriented Components to Protected Module Architectures

  2013influential citation
• The marriage of bisimulations and Kripke logical relations

  2012cites this paper
• Research Statement

  2010cites this paper
• Internship Topics on SECOMP: Formally Secure Compilation of Compartmentalized C Programs

  year unknowncites this paper
• Compiler Verification Meets Cross-Language Linking via Data Abstraction

  year unknowncites this paper
• Formally Secure Compilation Last

  year unknowncites this paper