4,738 research outputs found
Interview with Sam Lindley
Full text linkA former schoolteacher and retired librarian recalls the activities of the Friends (Quakers) in Hawaii during World War II. Lindley, of Caucasian ancestry, also relates meeting and marrying his Chinese wife.schoolteacher, librarian; Caucasian; maleInterview conducted in English.State, Federa
Foundations for programming and implementing effect handlers
Full text linkFirst-class control operators provide programmers with an expressive and efficient
means for manipulating control through reification of the current control state as a first-class object, enabling programmers to implement their own computational effects and
control idioms as shareable libraries. Effect handlers provide a particularly structured
approach to programming with first-class control by naming control reifying operations
and separating from their handling.
This thesis is composed of three strands of work in which I develop operational
foundations for programming and implementing effect handlers as well as exploring
the expressive power of effect handlers.
The first strand develops a fine-grain call-by-value core calculus of a statically
typed programming language with a structural notion of effect types, as opposed to the
nominal notion of effect types that dominates the literature. With the structural approach,
effects need not be declared before use. The usual safety properties of statically typed
programming are retained by making crucial use of row polymorphism to build and
track effect signatures. The calculus features three forms of handlers: deep, shallow,
and parameterised. They each offer a different approach to manipulate the control state
of programs. Traditional deep handlers are defined by folds over computation trees,
and are the original con-struct proposed by Plotkin and Pretnar. Shallow handlers are
defined by case splits (rather than folds) over computation trees. Parameterised handlers
are deep handlers extended with a state value that is threaded through the folds over
computation trees. To demonstrate the usefulness of effects and handlers as a practical
programming abstraction I implement the essence of a small UNIX-style operating
system complete with multi-user environment, time-sharing, and file I/O.
The second strand studies continuation passing style (CPS) and abstract machine
semantics, which are foundational techniques that admit a unified basis for implementing deep, shallow, and parameterised effect handlers in the same environment. The
CPS translation is obtained through a series of refinements of a basic first-order CPS
translation for a fine-grain call-by-value language into an untyped language. Each refinement moves toward a more intensional representation of continuations eventually
arriving at the notion of generalised continuation, which admit simultaneous support for
deep, shallow, and parameterised handlers. The initial refinement adds support for deep
handlers by representing stacks of continuations and handlers as a curried sequence of
arguments. The image of the resulting translation is not properly tail-recursive, meaning some function application terms do not appear in tail position. To rectify this the
CPS translation is refined once more to obtain an uncurried representation of stacks
of continuations and handlers. Finally, the translation is made higher-order in order to
contract administrative redexes at translation time. The generalised continuation representation is used to construct an abstract machine that provide simultaneous support for
deep, shallow, and parameterised effect handlers. kinds of effect handlers.
The third strand explores the expressiveness of effect handlers. First, I show that
deep, shallow, and parameterised notions of handlers are interdefinable by way of typed
macro-expressiveness, which provides a syntactic notion of expressiveness that affirms
the existence of encodings between handlers, but it provides no information about the
computational content of the encodings. Second, using the semantic notion of expressiveness I show that for a class of programs a programming language with first-class
control (e.g. effect handlers) admits asymptotically faster implementations than possible in a language without first-class control
Letter from Hayao (Sam) Chuman to the American Friends Service Committee
No full textA letter from Hayao (Sam) Chuman to the American Friends Service Committee, donating a portion of his redress check from the U.S. government to the Committee.The Chuman (Hayao "Sam" and Toshiko) Papers documents the World War II experiences of Hayao "Sam" and Toshiko Chuman, who were Kibei Nisei born in the United States but grew up and completed school in Japan, and then returned to the U.S. prior to the war. It chronicles the Chuman's incarceration from the Santa Anita Assembly Center, through Jerome, Rohwer, Tule Lake camps, and the Santa Fe and Crystal City internment camps as well as their struggle for restoring their U.S. citizenships in the 1960s. The digital collection consists of mostly textual material, including correspondence, affidavits, incarceration camp records, lease agreements, financial documents, receipts, pamphlets, and booklets
Letter from Hayao (Sam) Chuman to Earl Warren and "Attorney General Clark"
No full textA letter from Hayao (Sam) Chuman to Chief Justice of the Supreme Court Earl Warren and "Attorney General Clark". The letter is a request to regain his citizenship after renouncing his U.S. citizenship and requesting repatriation to Japan during his time incarcerated in World War II.The Chuman (Hayao "Sam" and Toshiko) Papers documents the World War II experiences of Hayao "Sam" and Toshiko Chuman, who were Kibei Nisei born in the United States but grew up and completed school in Japan, and then returned to the U.S. prior to the war. It chronicles the Chuman's incarceration from the Santa Anita Assembly Center, through Jerome, Rohwer, Tule Lake camps, and the Santa Fe and Crystal City internment camps as well as their struggle for restoring their U.S. citizenships in the 1960s. The digital collection consists of mostly textual material, including correspondence, affidavits, incarceration camp records, lease agreements, financial documents, receipts, pamphlets, and booklets
Mixing Metaphors: Actors as Channels and Channels as Actors
Full text linkChannel- and actor-based programming languages are both used in practice, but the two are often confused. Languages such as Go provide anonymous processes which communicate using buffers or rendezvous points—known as channels—while languages such as Erlang provide addressable processes—known as actors—each with a single incoming message queue. The lack of a common representation makes it difficult to reason about translations that exist in the folklore. We define a calculus λch for typed asynchronous channels, and a calculus λact for typed actors. We define translations from λact into λch and λch into λact and prove that both are type- and semantics preserving. We show that our approach accounts for synchronisation and selective receive in actor systems and discuss future extensions to support guarded choice and behavioural types
Conflation confers concurrency
Full text linkSession types provide a static guarantee that concurrent programs respect communication protocols. Recent work has explored a correspondence between proof rules and cut reduction in linear logic and typing and evaluation of process calculi. This paper considers two approaches to extend logically-founded process calculi. First, we consider extensions of the process calculus to more closely resemble π-calculus. Second, inspired by denotational models of process calculi, we consider conflating dual types. Most interestingly, we observe that these approaches coincide: conflating the multiplicatives (⊗ and
⅋) allows processes to share multiple channels; conflating the additives (⊕ and &) provides nondeterminism; and conflating the exponentials (! and ?) yields access points, a rendezvous mechanism for initiating session typed communication. Access points are particularly expressive: for example, they are sufficient to encode concurrent state and general recursion
Sam "Kangaroo"
Full text linkabstract: Sam left Sudan when he was six years old. He also witnessed many people die when they tried to cross the Gilo river.
“Lost Boys Found” is an ongoing, interdisciplinary project that is collecting, recording and archiving the oral histories of the Lost Boys/Girls of Sudan. The collection is a work-in-progress, seeking to record the oral history of as many Lost Boys/Girls as are willing, and will be used in a future book.Age: 23Region: Upper Nile (Bor)This picture and bio was donated to the "Lost Boys Found" oral history project from The Arizona Lost Boys Cente
the beat report piece detailing author Sam Pfeifle\u27s wishes for local music fo
No full textthe beat report piece detailing author Sam Pfeifle\u27s wishes for local music for 2004, mentioning radio stations WCYY and WCLZ, local band 6gig, and the Musicians Resource League
Separating Sessions Smoothly
Full text linkThis paper introduces Hypersequent GV (HGV), a modular and extensible core calculus for functional programming with session types that enjoys deadlock freedom, confluence, and strong normalisation. HGV exploits hyper-environments, which are collections of type environments, to ensure that structural congruence is type preserving. As a consequence we obtain a tight operational correspondence between HGV and HCP, a hypersequent-based process-calculus interpretation of classical linear logic. Our translations from HGV to HCP and vice-versa both preserve and reflect reduction. HGV scales smoothly to support Girard’s Mix rule, a crucial ingredient for channel forwarding and exceptions
Normalisation by Evaluation in the Compilation of Typed Functional Programming Languages
Full text linkThis thesis presents a critical analysis of normalisation by evaluation as a technique for
speeding up compilation of typed functional programming languages. Our investigation
focuses on the SML.NET compiler and its typed intermediate language MIL. We
implement and measure the performance of normalisation by evaluation for MIL across
a range of benchmarks. Taking a different approach, we also implement and measure
the performance of a graph-based shrinking reductions algorithm for SML.NET.
MIL is based on Moggi’s computational metalanguage. As a stepping stone to
normalisation by evaluation, we investigate strong normalisation of the computational
metalanguage by introducing an extension of Girard-Tait reducibility. Inspired by previous
work on local state and parametric polymorphism, we define reducibility for
continuations and more generally reducibility for frame stacks. First we prove strong
normalistion for the computational metalanguage. Then we extend that proof to include
features of MIL such as sums and exceptions.
Taking an incremental approach, we construct a collection of increasingly sophisticated
normalisation by evaluation algorithms, culminating in a range of normalisation
algorithms for MIL. Congruence rules and alpha-rules are captured by a compositional
parameterised semantics. Defunctionalisation is used to eliminate eta-rules. Normalisation
by evaluation for the computational metalanguage is introduced using a monadic
semantics. Variants in which the monadic effects are made explicit, using either state
or control operators, are also considered.
Previous implementations of normalisation by evaluation with sums have relied
on continuation-passing-syle or control operators. We present a new algorithm which
instead uses a single reference cell and a zipper structure. This suggests a possible
alternative way of implementing Filinski’s monadic reflection operations.
In order to obtain benchmark results without having to take into account all of
the features of MIL, we implement two different techniques for eliding language constructs.
The first is not semantics-preserving, but is effective for assessing the efficiency
of normalisation by evaluation algorithms. The second is semantics-preserving,
but less flexible. In common with many intermediate languages, but unlike the computational
metalanguage, MIL requires all non-atomic values to be named. We use either
control operators or state to ensure each non-atomic value is named.
We assess our normalisation by evaluation algorithms by comparing them with a
spectrum of progressively more optimised, rewriting-based normalisation algorithms.
The SML.NET front-end is used to generate MIL code from ML programs, including
the SML.NET compiler itself. Each algorithm is then applied to the generated MIL
code. Normalisation by evaluation always performs faster than the most naıve algorithms—
often by orders of magnitude. Some of the algorithms are slightly faster than
normalisation by evaluation. Closer inspection reveals that these algorithms are in fact
defunctionalised versions of normalisation by evaluation algorithms.
Our normalisation by evaluation algorithms perform unrestricted inlining of functions.
Unrestricted inlining can lead to a super-exponential blow-up in the size of
target code with respect to the source. Furthermore, the worst-case complexity of
compilation with unrestricted inlining is non-elementary in the size of the source code.
SML.NET alleviates both problems by using a restricted form of normalisation based
on Appel and Jim’s shrinking reductions. The original algorithm is quadratic in the
worst case. Using a graph-based representation for terms we implement a compositional
linear algorithm. This speeds up the time taken to perform shrinking reductions
by up to a factor of fourteen, which leads to an improvement of up to forty percent in
total compile time
- …
