Typing first-class continuations in ML

No abstract is available for this paper.

• Publication year

  1991

• Venue

  ACM-SIGACT Symposium on Principles of Programming Languages

• Publication date

  1991-01-03

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1145/99583.99608
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Imperative functional programming

  1993cited by this paper
• Polymorphic type assignment and CPS conversion

  1993cited by this paper
• Co-Induction in Relational Semantics

  1991cited by this paper
• Type Systems for Programming Languages

  1991cited by this paper
• Formal description of programming concepts

  1991cited by this paper
• Standard ML of New Jersey

  1991influential reference
• JFP volume 1 issue 4 Cover and Back matter

  1991cited by this paper
• Adding threads to Standard ML

  1990cited by this paper
• Asynchronous Signals is Standard ML

  1990cited by this paper
• Type Inference for Polymorphic References

  1990influential reference
• Definition of standard ML

  1990cited by this paper
• Reasoning with continuations II: full abstraction for models of control

  1990cited by this paper
• Declarative Continuations and Categorical Duality

  1989influential reference
• First-Class Synchronous Operations in Standard ML

  1989cited by this paper
• Continuation-passing, closure-passing style

  1989cited by this paper
• A formulae-as-type notion of control

  1989cited by this paper
• Engines From Continuations

  1989cited by this paper
• The theory and practice of first-class prompts

  1988cited by this paper
• Operational Semantics and Polymorphic Type Inference

  1988cited by this paper
• A Syntactic Theory of Sequential Control

  1987cited by this paper
• Embedding continuations in procedural objects

  1987cited by this paper
• Abstracting Timed Preemption with Engines

  1987cited by this paper
• Control operators, the SECD-machine, and the λ-calculus

  1987influential reference
• Reasoning with Continuations

  1986cited by this paper
• Rum. An Intensional Theory of Function and Control Abstractions

  1986cited by this paper
• A scheme for a higher-level semantic algebra

  1986cited by this paper
• Obtaining Coroutines with Continuations

  1986cited by this paper
• Logic Continuations

  1986cited by this paper
• Logical Relations and the Typed lambda-Calculus

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

  1985influential reference
• Algebraic Methods in Semantics

  1985cited by this paper
• Natural semantics on the computer

  1984cited by this paper
• Programming with Continuations

  1984cited by this paper
• The Completeness Theorem for Typing lambda-Terms

  1983cited by this paper
• Principal type-schemes for functional programs

  1982influential reference
• Continuation-Based Multiprocessing

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

  1978cited by this paper
• An Interpreter for Extended Lambda Calculus

  1975cited by this paper
• On the Relation between Direct and Continuation Semantics

  1974influential reference
• Definitional Interpreters for Higher-Order Programming Languages

  1972influential reference
• GEDANKEN—a simple typeless language based on the principle of completeness and the reference concept

  1970cited by this paper
• PAL—a language designed for teaching programming linguistics

  1968cited by this paper
• Correspondence between ALGOL 60 and Church's Lambda-notation

  1965cited by this paper

• The Duality of λ-Abstraction

  2025cites this paper
• A General Fine-Grained Reduction Theory for Effect Handlers

  2023cites this paper
• Call-by-push-value

  2022cites this paper
• On Correspondence between Selective CPS Transformation and Selective Double Negation Translation

  2021influential citation
• Reachability types: tracking aliasing and separation in higher-order functional programs

  2021cites this paper
• The history of Standard ML

  2020cites this paper
• Compiling with continuations, or without? whatever.

  2019cites this paper
• Sequential Effect Systems with Control Operators

  2018cites this paper
• Analytical Approach to Programs as Data Objects

  2017cites this paper
• A verified abstract machine for functional coroutines

  2016cites this paper
• Towards flexible goal-oriented logic programming

  2016cites this paper
• Game Semantics for Type Soundness

  2015cites this paper
• Research Showcase @ CMU

  2015cites this paper
• A Dynamic Continuation-Passing Style for Dynamic Delimited Continuations

  2015cites this paper
• PhD Abstracts

  2015cites this paper
• A A Dynamic Continuation-Passing Style for Dynamic Delimited

  2014cites this paper
• Substitution, jumps, and algebraic effects

  2014cites this paper
• Operational Semantics of Functional Languages

  2014cites this paper
• Implementing LP Systems with CP Techniques

  2013cites this paper
• Proving termination of evaluation for System F with control operators

  2013influential citation
• Delimited continuations in Prolog: semantics, use, and implementation in the WAM

  2013cites this paper
• Linear and Affine Typing of Continuation-Passing Style

  2013cites this paper
• Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control

  2012cites this paper
• Interruptible context-dependent executions: a fresh look at programming context-aware applications

  2012cites this paper
• Typing control operators in the CPS hierarchy

  2011cites this paper
• Subtyping delimited continuations

  2011cites this paper
• A program logic for higher-order procedural variables and non-local jumps

  2011cites this paper
• Typing Coroutines

  2010cites this paper
• Context-based proofs of termination for typed delimited-control operators

  2009cites this paper
• Program Logics for Sequential Higher-Order Control

  2009cites this paper
• Revisiting coroutines

  2009cites this paper
• A Context-based Approach to Proving Termination of Evaluation

  2009influential citation
• Towards Compatible and Interderivable Semantic Specifications for the Scheme Programming Language, Part I: Denotational Semantics, Natural Semantics, and Abstract Machines

  2008influential citation
• Curry-Howard Term Calculi for Gentzen-Style Classical Logics

  2008cites this paper
• Defunctionalized interpreters for programming languages

  2008cites this paper
• A syntactic correspondence between context-sensitive calculi and abstract machines

  2007cites this paper
• Polymorphic Delimited Continuations

  2007cites this paper
• The Theory and Practice of Programming Languages with Delimited Continuations

  2007influential citation
• The case of lambda expressions (Rule 17) shows how memory allocation is handled.

  2007cites this paper
• The Formal Speciication of Programming Languages Thesis Advisor: Committee

  2007cites this paper
• Combining algebraic effects with continuations

  2007cites this paper
• Substructural Simple Type Theories for Separation and In-place Update

  2006cites this paper
• Chapter 6 - Classical logic and control operators

  2006cites this paper
• Relational parametricity and control

  2005cites this paper
• A programming language for probabilistic computation

  2005cites this paper
• A Syntactic Correspondence between Context-Sensitive Calculi and Abstract Machines

  2005cites this paper
• Normalisation by evaluation in the compilation of typed functional programming languages

  2005cites this paper
• On the dynamic extent of delimited continuations

  2005cites this paper
• A Dynamic Continuation-Passing Style for Dynamic Delimited Continuations

  2005cites this paper
• On the static and dynamic extents of delimited continuations

  2005cites this paper
• Self-Aware Software - Will It Become a Reality?

  2005cites this paper
• Adding imperative programming to the pattern calculus

  2005influential citation
• A Type Theory for Krivine-Style Evaluation and Compilation

  2004cites this paper
• On the call-by-value CPS transform and its semantics

  2004cites this paper
• A Logical View of Effects

  2004cites this paper
• Functional programming with names and necessity

  2004cites this paper
• A Formulae-as-Types Interpretation of Subtractive Logic

  2004cites this paper
• From control effects to typed continuation passing

  2003cites this paper
• Minimal Classical Logic and Control Operators

  2003cites this paper
• Unwind-protect in portable Scheme

  2003cites this paper
• Offline partial evaluation for shift and reset

  2002cites this paper
• LISP AND SYMBOLIC COMPUTATION : An International Journal , ? , ? ? – ? ?

  2002influential citation
• Online partial evaluation for shift and reset

  2002cites this paper
• Type Systems in Programming Languages

  2002cites this paper
• Value recursion in monadic computations

  2002cites this paper
• Contrasting Exceptions and Continuations

  2001cites this paper
• Exceptional Syntax

  2001cites this paper
• Axioms for Recursion in Call-by-Value (Extended Abstract)

  2001cites this paper
• Operational Interpretations of an Extension of F ! with Control Operatorsy Capsule Review

  2001cites this paper
• Axioms for Recursion in Call-by-Value

  2001cites this paper
• Extensible virtual machines

  2001cites this paper
• A Selective CPS Transformation

  2001cites this paper
• Domain-Free ??-Calculus

  2000cites this paper
• A Type-Theoretic Study on Partial Continuations

  2000cites this paper
• Search algorithms in type theory

  2000cites this paper
• Interpreting Functions as Pi-Calculus Processes: A Tutorial

  1999cites this paper
• Using a Continuation Twice and Its Implications for the Expressive Power of call/cc

  1999cites this paper
• A Classical Linear lambda-Calculus

  1999cites this paper
• Representing layered monads

  1999cites this paper
• Formalizing Implementation Strategies for First-Class Continuations

  1999cites this paper
• Explicitly Typed lambda µ-Calculus for Polymorphism an Call-by-Value

  1999influential citation
• Call-by-Push-Value: A Subsuming Paradigm

  1999cites this paper
• A semantic analysis of control

  1999cites this paper
• Relational Interpretations of Recursive Types in an Operational Setting

  1999cites this paper
• Operational reasoning for functions with local state

  1999cites this paper
• From λ to π; or, Rediscovering continuations

  1999cites this paper
• CPS Translations and Applications: The Cube and Beyond

  1999cites this paper
• Polymorphic Call-by-Value Calculus Based on Classical Proofs

  1998cites this paper
• An Operational Investigation of the CPS Hierarchy

  1998cites this paper
• An Introduction to Landin's “A Generalization of Jumps and Labels”

  1998cites this paper
• Reactive programming in Standard ML

  1998cites this paper
• Definitional Interpreters Revisited

  1998cites this paper
• Return Types for Functional Continuations

  1998cites this paper
• Return Types for Functional Continuations

  1998influential citation
• A notion of classical pure type system

  1997influential citation
• Relational Interpretations of Recursive Types in an operational Setting (Summary)

  1997cites this paper
• Environments, Continuation Semantics and Indexed Categories

  1997cites this paper
• A Curry-Howard foundation for functional computation with control

  1997cites this paper
• Continuation semantics and self-adjointness

  1997cites this paper
• Calculus of Classical Proofs I

  1997cites this paper