Small-step and big-step semantics for call-by-need (2009)
Nakata, Keiko, Hasegawa, Masahito
We present natural semantics for acyclic as well as cyclic call-by-need lambda calculi, which are proved equivalent to the reduction semantics given by Ariola and Felleisen. The natural semantics are...
Axioms for Recursion in Call-by-Value (Extended Abstract) (2008)
Masahito Hasegawa, Yoshihiko Kakutani
Abstract. We propose an axiomatization of fixpoint operators in typed call-by-value programming languages, and give its justifications in two ways. First, it is shown to be sound and complete for the...
Finite Dimensional Vector Spaces are Complete for Traced Symmetric Monoidal Categories (2008)
Masahito Hasegawa, Martin Hofmann, Gordon Plotkin
Abstract. We show that the category FinVectk of finite dimensional vector spaces and linear maps over any field k is (collectively) complete for the traced symmetric monoidal category freely...
Axioms for Recursion in Call-by-Value (Extended Abstract) (2007)
Masahito Hasegawa, Yoshihiko Kakutani
Abstract. We propose an axiomatization of fixpoint operators in typed call-by-value programming languages, and give its justifications in two ways. First, it is shown to be sound and complete for the...
Axioms for Recursion in Call-by-Value (Extended Abstract) (2007)
Masahito Hasegawa, Yoshihiko Kakutani
We propose an axiomatization of the fixpoint operators in the typed call-by-value programming languages, and give its justifications in two ways. First, it is shown to be sound and complete for the...
Proposed Running Head: Higher-Order and Reflexive Action Calculi Corresponding Author: (2007)
Masahito Hasegawa, Masahito Hasegawa
Action calculi have been introduced by Milner as a framework for representing models of interactive behaviour. Two natural extensions of action calculi have been proposed: the higher-order action...
f!;(g is Full in f!; (g (2007)
Masahito Hasegawa Rims, Masahito Hasegawa
We show that the f!;(g-fragment of Intuitionistic Linear Logic is full in the f!; (g-fragment, both formulated as linear lambda calculi. The proof is a mild extension of our previous technique used...
Relational Parametricity and Control (2006)
We study the equational theory of Parigot's second-order λμ-calculus in connection with a call-by-name continuation-passing style (CPS) translation into a fragment of the second-order...
A terminating and confluent linear lambda calculus (2006)
Abstract. We present a rewriting system for the linear lambda calculus corresponding to the {!, ⊸}-fragment of intuitionistic linear logic. This rewriting system is shown to be strongly...
Parameterizations and Fixed-Point Operators on Control Categories (2005)
Yoshihiko Kakutani, Masahito Hasegawa
The #-calculus features both variables and names, together with their binding mechanisms. This means that constructions on open terms are necessarily parameterized in two di#erent ways for both...
The uniformity principle on traced monoidal categories (2004)
The uniformity principle for traced monoidal categories has been introduced as a natural generalization of the uniformity principle (Plotkin's principle) for fixpoint operators in domain theory. We...
Semantics of linear continuation-passing in call-by-name (2004)
Abstract. We propose a semantic framework for modelling the linear usage of continuations in typed call-by-name programming languages. On the semantic side, we introduce a construction for categories...
Coherence of the Double Negation in Linear Logic (Algebra, Logic and Geometry in Informatics) (2003)
The Uniformity Principle on Traced Monoidal Categories (2003)
The uniformity principle for traced monoidal categories has been introduced as a natural generalization of the uniformity principle (Plotkin's principle) for fixpoint operators in domain theory....
The uniformity principle on traced monoidal categories (2003)
The uniformity principle for traced monoidal categories has been introduced as a natural generalization of the uniformity principle (Plotkin’s principle) for fixpoint operators in domain theory. We...
A Sound and Complete Axiomatization of Delimited Continuations (2003)
Yukiyoshi Kameyama, Masahito Hasegawa
The shift and reset operators, proposed by Danvy and Filinski, are powerful control primitives for capturing delimited continuations. Delimited continuation is a similar concept as the standard...
The uniformity principle on traced monoidal categories (2003)
The uniformity principle for traced monoidal categories has been introduced as a natural generalization of the uniformity principle (Plotkin’s principle) for fixpoint operators in domain theory. We...
Axioms for recursion in call-by-value (2002)
Masahito Hasegawa, Yoshihiko Kakutani
Abstract. We propose an axiomatization of fixpoint operators in typed call-byvalue programming languages, and give its justifications in two ways. First, it is shown to be sound and complete for the...
Axioms for recursion in call-by-value (2002)
Masahito Hasegawa, Yoshihiko Kakutani
Abstract. We propose an axiomatization of xpoint operators in typed call-byvalue programming languages, and give its justications in two ways. First, it is shown to be sound and complete for the...
Classical linear logic of implications (2002)
Abstract. We give a simple term calculus for the multiplicative exponential fragment of Classical Linear Logic, by extending Barber and Plotkin’s system for the intuitionistic case. The calculus...
Linearly Used Effects: Monadic and CPS Transformations into the Linear Lambda Calculus (2002)
Abstract. We propose a semantic and syntactic framework for modelling linearly used effects, by giving the monadic transforms of the computational lambda calculus (considered as the core calculus of...
Linearly Used Effects: Monadic and CPS Transformations into the Linear Lambda Calculus (2002)
We propose a semantic and syntactic framework for modelling linearly used effects, by giving the monadic transforms of the computational lambda calculus (considered as the core calculus of typed...
Classical Linear Logic of Implications (2002)
We give a simple term calculus for the multiplicative exponential fragment of Classical Linear Logic, by extending Barber and Plotkin's system for the intuitionistic case. The calculus has the...
Glueing Algebraic Structures on a 2-Category (2000)
We study the glueing constructions (comma objects) on general algebraic structures on a 2-category, described in terms of 2-monads and adjunctions. Specifically, lifting theorems for the comma...
Girard Translation and Logical Predicates (2000)
We present a short proof of a folklore result: the Girard translation from the simply typed lambda calculus to the linear lambda calculus is fully complete. The proof makes use of a notion of logical...
Logical Predicates for Intuitionistic Linear Type Theories (1999)
We develop a notion of Kripke-like parameterized logical predicates for two fragments of intuitionistic linear logic (MILL and DILL) in terms of their category-theoretic models. Such logical...
Categorical Glueing and Logical Predicates for Models of Linear Logic (1999)
We give a series of glueing constructions for categorical models of fragments of linear logic. Specifically, we consider the glueing of (i) symmetric monoidal closed categories (models of...
Categorical glueing and logical predicates for models of linear logic (1999)
We give a series of glueing constructions for categorical models of fragments of linear logic. Specifically, we consider the glueing of (i) symmetric monoidal closed categories (models of...
Cover title.
From Action Calculi to Linear Logic (1998)
Barber, Andrew G, Gardner, Phillipa, Hasegawa, Masahito, Plotkin, Gordon
Milner introduced action calculi as a framework for investigating models of interactive behaviour. We present a type-theoretic account of action calculi using the propositions-as-types paradigm; the...
From Action Calculi to Linear Logic (1998)
Barber, Andrew G, Gardner, Phillipa, Hasegawa, Masahito, Plotkin, Gordon
Milner introduced action calculi as a framework for inves- tigating models of interactive behaviour. We present a type-theoretic account of action calculi using the propositions-as-types paradigm;...
From Action Calculi to Linear Logic (1998)
Andrew Barber, Philippa Gardner, Masahito Hasegawa, Gordon Plotkin
. Milner introduced action calculi as a framework for investigating models of interactive behaviour. We present a type-theoretic account of action calculi using the propositions-as-types paradigm;...
Models of Cyclic Structures: Knots, Term Graphs, and Recursion (1998)
n Categorical Rewriting Again such a question is not easy (both to ask and to answer), if we just look at graphs; following Ariola and Klop, cyclic lambda calculi essentially lack the confluence...
From action calculi to linear logic (1998)
Andrew Barber, Masahito Hasegawa, Gordon Plotkin
Abstract. Milner introduced action calculi as a framework for investigating models of interactive behaviour. We present a type-theoretic account of action calculi using the propositions-as-types...
Types and Models for Higher-Order Action Calculi (1997)
Philippa Gardner, Masahito Hasegawa
. Milner introduced action calculi as a framework for representing models of interactive behaviour. He also introduced the higherorder action calculi, which add higher-order features to the basic...
Recursion from Cyclic Sharing: Traced Monoidal Categories and Models of Cyclic Lambda Calculi (1997)
. Cyclic sharing (cyclic graph rewriting) has been used as a practical technique for implementing recursive computation efficiently. To capture its semantic nature, we introduce categorical models...
Models of Sharing Graphs: A Categorical Semantics of let and letrec (1997)
To my parents A general abstract theory for computation involving shared resources is presented. We develop the models of sharing graphs, also known as term graphs, in terms of both syntax and...
Decomposing Typed Lambda Calculus Into a Couple of Categorical Programming Languages (1995)
. We give two categorical programming languages with variable arrows and associated abstraction/reduction mechanisms, which extend the possibility of categorical programming [Hag87, CF92] in...