Quantum Circuits: From a Network to a One-Way Model (2009)
Larisse D. Voufo, Gerardo Ortiz, Amr Sabry
We present elements of quantum circuits translations from the standard network (or circuit) model to the one-way one. We present a general translation scheme, give an account of currently existing...
Larisse D. Voufo, Gerardo Ortiz, Amr Sabry
Abstract—We present elements of quantum circuits translations from the (standard) network or circuit model to the one-way one. We present a translation scheme, give an account of currently existing...
The Arrow Calculus as a Quantum Programming Language (2009)
Vizzotto, Juliana Kaizer, Bois, Andre Rauber Du, Sabry, Amr
We express quantum computations (with measurements) using the arrow calculus extended with monadic constructions. This framework expresses quantum programming using well-understood and familiar...
zDepartment of Computer ScienceYale University
QPL 2005 Preliminary Version An Algebra of Pure Quantum Programming Abstract (2008)
Thorsten Altenkirch, Jonathan Grattage, Juliana K. Vizzotto, Amr Sabry
We develop a sound and complete equational theory for the functional quantum programming language QML. The soundness and completeness of the theory are with respect to the previously-developed...
QPL 2005 Preliminary Version An Algebra of Pure Quantum Programming Abstract (2008)
Thorsten Altenkirch, Jonathan Grattage, Juliana K. Vizzotto, Amr Sabry
We develop a sound and complete equational theory for the functional quantum programming language QML. The soundness and completeness of the theory are with respect to the previously developed...
John Fiskio-lasseter, Amr Sabry
We present a syntactic theory for the behavioral subset of the Verilog Hardware Description Language. Due to the complexity of the language, the construction of this theory represents a serious test...
Abstract The Essence of Compiling with Continuations (2008)
Cormac Flanagan, Amr Sabry, Bruce F. Duba, Matthias Felleisen
In order to simplify the compilation process, many compilers for higher-order languages use the continuationpassing style (CPS) transformation in a rst phase to generate an intermediate...
QPL 2005 Preliminary Version An algebra of pure quantum programming Abstract (2008)
Thorsten Altenkirch, Jonathan Grattage, Juliana K. Vizzotto, Amr Sabry
We develop a sound and complete equational theory for the functional quantum programming language QML. The soundness and completeness of the theory are with respect to the previously-developed...
zDepartment of Computer ScienceYale University
QPL 2006 Preliminary Version Quantum arrows in Haskell (2008)
Juliana Kaizer, Vizzotto Antônio, Carlos Rocha Costa, Amr Sabry
We argue that a realistic model for quantum computations should be general with respect to measurements, and complete with respect to the information flow between the quantum and classical worlds. We...
A Monadic Framework for Delimited Continuations (2008)
R. Kent, Dybvig Simon, Peyton Jones, Amr Sabry
Delimited continuations are more expressive than traditional abortive continuations and they apparently require a framework beyond traditional continuation-passing style (CPS). We show that this is...
Abstract. This paper proposes an operational semantics for value recursion in the context of monadic metalanguages. Our technique for combining value recursion with computational effects works...
Computational Content of Unique Decomposition Proofs (2007)
Syntax (e.g., ELF) since one cannot represent evaluation contexts as meta-functions. Second one cannot use just one metavariable to describe the goal type E[x] as before. A crucial proof step in the...
Declarative Programming Across the Undergraduate Curriculum (2007)
In its ultimate form, declarative programming provides solutions to problems using only a statement of the problem as the program. Historically this level of abstraction has been associated with...
THEORET I CAL PEARLS CPS in Little Pieces: Composing Partial Continuations (2007)
This paper presents a new two-stage CPS algorithm. The first stage plants trivial partial continuations via a recursive-descent traversal and the second stage is a rewrite system that terminates when...
Declarative Programming Across the Undergraduate Curriculum (2007)
In its ultimate form, declarative programming provides solutions to problems using only a statement of the problem as the program. Historically this level of abstraction has been associated with...
THEORET I CAL PEARLS CPS in Little Pieces: Composing Partial Continuations (2007)
This paper presents a new two-stage CPS algorithm. The first stage plants trivial partial continuations via a recursive-descent traversal and the second stage is a rewrite system that transforms all...
John Fiskio-lasseter, Amr Sabry
We present a syntactic theory for the behavioral subset of the Verilog Hardware Description Language. Due to the complexity of the language, the construction of this theory represents a serious test...
The widespread use of the continuation-passing style (CPS) transformation in compilers, optimizers, abstract interpreters, and partial evaluators reflects a common belief that the transformation has...
The-calculus is the simple and elegant, yet powerful basis for the semantic manipulation of functional programs by programmers and programming tools (compilers, optimizers, semantics-based editors)...
The widespread use of the continuation-passing style (CPS) transformation in compilers, partial evaluators, and abstract interpretations suggests that it is useful for program analysis. Indeed, there...
Title: A TYPE-AND-EFFECT SYSTEM FOR ENCAPSULATING MEMORY IN JAVA (2007)
Bennett Norton Yates, Dr. Amr Sabry
ii
1 A Reflection on Call-by-Value (2007)
Amr Sabry, Amr Sabry, Philip Wadler, Philip Wadler
A number of compilers exploit the following strategy: translate a term to continuationpassing style (CPS) and optimize the resulting term using a sequence of reductions. Recent work suggests that an...
We describe a gap in Java's security model that allows a pure Java library to infer information to which it should not have access. The security violation exploits two pieces of public...
Title: A FORMAL DESCRIPTION OF BEHAVIORAL VERILOG BASED ON AXIOMATIC SEMANTICS (2007)
John Howard, Eli Fiskio-lasseter, Dr. Amr Sabry
Reasoning about hardware designs written in Verilog is problematic, in large part because of the lack of a formal semantics for the language. The behavioral aspects of many constructs within the...
A Type-Theoretic Foundation of Delimited Continuations (2007)
Ariola, Zena, Herbelin, Hugo, Sabry, Amr
There is a correspondence between classical logic and programming language calculi with first-class continuations. With the addition of control delimiters, the continuations become composable and the...
A Type-Theoretic Foundation of Delimited Continuations (2007)
Ariola, Zena, Herbelin, Hugo, Sabry, Amr
There is a correspondence between classical logic and programming language calculi with first-class continuations. With the addition of control delimiters, the continuations become composable and the...
An Algebra of Pure Quantum Programming (2005)
Altenkirch, Thorsten, Grattage, Jonathan, Vizzotto, Juliana K., Sabry, Amr
We develop a sound and complete equational theory for the functional quantum programming language QML. The soundness and completeness of the theory are with respect to the previously-developed...
Zena M. Ariola, Hugo Herbelin, Amr Sabry, Zena M. Ariola, Hugo Herbelin, Amr Sabry
We give an analysis of various classical axioms and characterize a notion of minimal classical logic that enforces Peirce’s law without enforcing Ex Falso Quodlibet. We show that a “natural ”...
A monadic framework for delimited continuations (2005)
R. Kent Dybvig, Simon Peyton Jones, R. Kent, Dybvig Simon, Peyton Jones, Amr Sabry, ...
Delimited continuations are more expressive than traditional abortive continuations and they apparently seem to require a framework beyond traditional continuation-passing style (CPS). We show that...
A monadic framework for subcontinuations (2005)
R. Kent Dybvig, Simon Peyton Jones, Amr Sabry
Abstract. Functional and delimited continuations are more expressive than traditional abortive continuations and they apparently seem to require a framework beyond traditional continuation or monadic...
A Typed Calculus Supporting Shallow Embeddings of Abstract Machines 1 Overview (2005)
Aaron Bohannon, Zena M. Ariola, Amr Sabry
The goal of this work is to draw a formal connection between steps taken by abstract machines and reductions in a system of proof terms for a version the sequent calculus. We believe that by doing so...
From syntactic theories to interpreters: Automating the proof of unique decomposition (2004)
Yong Xiao, Amr Sabry, Zena M. Ariola
Abstract. Developing syntactic theories for reasoning about programming languages usually involves proving a unique-decomposition lemma. The proof of such a lemma is tedious, error-prone, and is...
From syntactic theories to interpreters: Automating the proof of unique decomposition (2004)
Yong Xiao, Amr Sabry, Zena Ariola
Abstract. Developing syntactic theories for reasoning about programming languages usually involves proving a unique decomposition lemma. The proof of such a lemma is tedious, and error-prone, and is...
An Abstract Monadic Semantics for Value Recursion (2003)
E. Moggi, Eugenio Moggi, Amr Sabry
MONADIC SEMANTICS FOR VALUE RECURSION #, ## Eugenio Moggi and Amr Sabry Abstract. This paper proposes an operational semantics for value recursion in the context of monadic metalanguages. Our...
Macros as multi-stage computations: Type-safe, generative, binding macros in MacroML (2001)
Steve Ganz, Amr Sabry, Walid Taha
Macros have traditionally been viewed as operations on syntax trees or even on plain strings. This view makes macros seem ad hoc, and is at odds with two desirable features of contemporary typed...
Monadic encapsulation of effects: A revised approach (extended version (2001)
Launchbury and Peyton Jones came up with an ingenious idea for embedding regions of imperative programming in a pure functional language like Haskell. The key idea was based on a simple modification...
Macros as multi-stage computations: Type-safe, generative, binding macros in MacroML (2001)
Steven E. Ganz, Amr Sabry, Walid Taha
With few exceptions, macros have traditionally been viewed as operations on syntax trees or even on plain strings. This view makes macros seem ad hoc, and is at odds with two desirable features of...
Macros as multi-stage computations: Type-safe, generative, binding macros in MacroML (2001)
Steve Ganz, Amr Sabry, Walid Taha
Macros have traditionally been viewed as operations on syntax trees or even on plain strings. This view makes macros seem ad hoc, and is at odds with two desirable features of contemporary typed...
Monadic encapsulation of effects: A revised approach (extended version (2001)
Launchbury and Peyton Jones came up with an ingenious idea for embedding regions of imperative programming in a pure functional language like Haskell. The key idea was based on a simple modification...
Monadic encapsulation of effects: A revised approach (extended version (2001)
Launchbury and Peyton Jones came up with an ingenious idea for embedding regions of imperative programming in a pure functional language like Haskell. The key idea was based on a simple modification...
Recursion is a computational effect (2000)
Daniel P. Friedman, Daniel P. Friedman, Amr Sabry, Amr Sabry
In a recent paper, Launchbury, Lewis, and Cook observe that some Haskell applications could benefit from a combinator mfix for expressing recursion over monadic types. We investigate three possible...
Recursion is a Computational E ect (2000)
Daniel P. Friedman, Amr Sabry, Daniel P. Friedman, Amr Sabry
In a recent paper, Launchbury, Lewis, and Cook observe that some Haskell applications could bene t from a combinator m x for expressing recursion over monadic types. We investigate three possible de...
Recursion is a Computational E ect (2000)
Daniel P. Friedman, Amr Sabry, Daniel P. Friedman, Amr Sabry
In a recent paper, Launchbury, Lewis, and Cook observe that some Haskell applications could bene t from a combinator m x for expressing recursion over monadic types. We investigate three possible de...
Monadic encapsulation in ML (1999)
In a programming language with procedures and assignments, it is often important to isolate uses of state to particular program fragments. The frameworks of type, region, and effect inference, and...
Monadic encapsulation of effects: A revised approach (Extended Version) (1999)
Launchbury and Peyton Jones came up with an ingenious idea for embedding regions of imperative programming in a pure functional language like Haskell. The key idea was based on a simple modication of...
Monadic Encapsulation in ML (1999)
In a programming language with procedures and assignments, it is often important to isolate uses of state to particular program fragments. The frameworks of type, region, and effect inference, and...
What is a purely functional language (1998)
Functional programming languages are informally classified into pure and impure languages. The precise meaning of this distinction has been a matter of controversy. We therefore investigate a formal...
Java access modifiers in parallel universes (1998)
This short note describes a gap in Java's access control mechanism that sometimes allows a Java class to illegally find the values of private variables in other classes.
Correctness of monadic state: an imperative call-by-need calculus (1998)
The extension of Haskell with a built-in state monad combines mathematical elegance with operational efficiency: ffl Semantically, at the source language level, constructs that act on the state are...
Correctness of Monadic State: An Imperative Call-by-Need Calculus (1998)
The extension of Haskell with a built-in state monad combines mathematical elegance with operational efficiency: ffl Semantically, at the source language level, constructs that act on the state are...
Monadic state: axiomatization and type safety (1997)
John Launchbury, Amr Sabry, When Launchbury
Type safety of imperative programs is an area fraught with difficulty and requiring great care. The SML solution to the problem, originally involving imperative type variables, has been recently...
Debugging reactive systems in haskell (1997)
We support the use of Haskell in two classes of applications. First, we note that although Haskell is well-suited for stream-oriented applications, like reactive systems, most implementations lack...
A reflection on call-by-value (1997)
A number of compilers exploit the following strategy: translate a term to continuation-passing style (CPS) and optimize the resulting term using a sequence of reductions. Recent work suggests that an...
Monadic state: axiomatization and type safety (1997)
John Launchbury, Amr Sabry, When Launchbury
Type safety of imperative programs is an area fraught with difficulty and requiring great care. The ML solution to the problem, originally involving imperative type variables, has recently been...
Debugging Reactive Systems in Haskell (1997)
This paper reports on the design and implementation of such a debugger in the context of the Haskell compiler `hbc.' The debugger has an intuitive graphical user interface, and can be used to...
Monadic State: Axiomatization and Type Safety (1997)
John Launchbury, Amr Sabry, When Launchbury
Type safety of imperative programs is an area fraught with difficulty and requiring great care. The SML solution to the problem, originally involving imperative type variables, has been recently...
Proving the correctness of reactive systems using sized types (1996)
John Hughes, Lars Pareto, Amr Sabry
{ rjmh, pareto, sabry We have designed and implemented a type-based analysis for proving some baaic properties of reactive systems. The analysis manipulates rich type expressions that contain...
Proving the correctness of reactive systems using sized types (1996)
John Hughes, Lars Pareto, Amr Sabry
We have designed and implemented a type-based analysis for proving some basic properties of reactive systems. The analysis manipulates rich type expressions that contain information about the sizes...
Proving the Correctness of Reactive Systems Using Sized Types (1996)
John Hughes, Lars Pareto, Amr Sabry
We have designed and implemented a type-based analysis for proving some basic properties of reactive systems. The analysis manipulates rich type expressions that contain information about the sizes...
Proving the Correctness of Reactive Systems Using Sized Types (1996)
John Hughes, Lars Pareto, Amr Sabry
We have designed and implemented a type-based analysis for proving some basic properties of reactive systems. The analysis manipulates rich type expressions that contain information about the sizes...
"August 1994."
Is continuation-passing useful for data flow analysis (1994)
The widespread use of the continuation-passing style interpreters, and partial evaluators reflects a common belief that the transformation has a positive effect on the analysis of programs....
Is Continuation-Passing Useful for Data Flow Analysis? (1994)
The widespread use of the continuation-passing style (CPS) transformation in compilers, optimizers, abstract interpreters, and partial evaluators reflects a common belief that the transformation has...
Reasoning about programs in continuation-passing style (1993)
Plotkin's-value calculus is sound but incomplete for reasoning about fij-transformations on programs in continuation-passing style (CPS). To find a complete extension, we define a new,...
The essence of compiling with continuations (1993)
Cormac Flanagan, Amr Sabry, Bruce F. Duba, Matthias Felleisen
In order to simplify the compilation process, many compilers for higher-order languages use the continuationpassing style (CPS) transformation in a first phase to generate an intermediate...
Reasoning about programs in continuation-passing style (1993)
Amr Sabry, Amr Sabry, Matthias Felleisen, Matthias Felleisen
Plotkin's-value calculus is sound but incomplete for reasoning about fij-transfor-mations on programs in continuation-passing style (CPS). To find a complete extension, we define a new,...
Reasoning about explicit and implicit representations of state (1993)
The semantics of imperative languages are often expressed in terms of a store-passing translation and an algebra for reasoning about stores. We axiomatize the semantics of several typical imperative...
The essence of compiling with continuations (1993)
Cormac Flanagan, Amr Sabry, Bruce F. Duba, Matthias Felleisen
In order to simplify the compilation process, many compilers for higher-order languages use the continuationpassing style (CPS) transformation in a first phase to generate an intermediate...
The Essence of Compiling with Continuations (1993)
Cormac Flanagan, Amr Sabry, Bruce F. Duba, Matthias Felleisen
In order to simplify the compilation process, many compilers for higher-order languages use the continuationpassing style (CPS) transformation in a first phase to generate an intermediate...
Reasoning about Explicit and Implicit Representations of State (1993)
The semantics of imperative languages are often expressed in terms of a store-passing translation and an algebra for reasoning about stores. We axiomatize the semantics of several typical imperative...
Retrospective on “The essence of compiling with continuations”, in (1979)
Continuation-passing style (CPS) became a popular intermediate representation for compilers of higher-order functional languages during the 1980’s (Rabbit [20], Orbit [13], SML/NJ [3, 4]). The...
Reasoning about Programs in Continuation-Passing Style
Amr Sabry, Amr Sabry, Matthias Felleisen, Matthias Felleisen
Plotkin's -value calculus is sound but incomplete for reasoning about fij-transfor- mations on programs in continuation-passing style (CPS). To find a complete extension, we define a new,...
Reasoning about Programs in Continuation-Passing Style
Plotkin's -value calculus is sound but incomplete for reasoning about fij-transformations on programs in continuation-passing style (CPS). To find a complete extension, we define a new,...