The search session has expired. Please query the service again.
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 uniformly for all monads. The operational nature of our approach is related to the implementation of recursion in Scheme and its monadic version proposed by Friedman and Sabry, but it defines a different semantics and does not rely on assignments. When contrasted to the axiomatic approach proposed by Erkök and Launchbury,...
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 uniformly for
all monads.
The operational nature of our approach is related to the
implementation of recursion in Scheme and its monadic version proposed
by Friedman and Sabry, but it defines a different semantics and does
not rely on assignments. When contrasted to the axiomatic approach
proposed by Erkök and Launchbury,...
Various static analyses of functional programming languages
that permit infinite data structures make use of set
constants like Top, Inf, and Bot, denoting
all terms, all lists not eventually ending in Nil, and
all non-terminating programs, respectively. We use a set
language that permits union, constructors and recursive
definition of set constants with a greatest fixpoint semantics
in the set of all, also infinite, computable trees,
where all term constructors are non-strict.
This...
We show that the standard normalization-by-evaluation construction for the simply-typed -calculus has a natural counterpart for the untyped -calculus, with the central type-indexed logical relation replaced by a “recursively defined” invariant relation, in the style of Pitts. In fact, the construction can be seen as generalizing a computational-adequacy argument for an untyped, call-by-name language to normalization instead of evaluation.In the untyped setting, not all terms have normal forms,...
We show that the standard normalization-by-evaluation construction for the
simply-typed λβη-calculus
has a natural counterpart for the untyped
λβ-calculus, with the central type-indexed logical relation
replaced by a “recursively defined” invariant relation, in
the style of Pitts. In fact, the construction can be seen as
generalizing a computational-adequacy argument for an untyped,
call-by-name language to normalization instead of evaluation.In the untyped setting, not all terms have normal...
We introduce a domain-free λµ-calculus of call-by-value
as a short-hand for the second order Church-style.
Our motivation comes from the observation that
in Curry-style polymorphic calculi, control operators such as
callcc-operators cannot, in general, handle correctly
the terms placed on the control operator's left, so that
the Curry-style system can fail to prove the subject reduction property.
Following the continuation semantics,
we also discuss the notion of values in classical system,...
Mainstream object-oriented
languages often fail to provide complete powerful features
altogether, such as, multiple inheritance, dynamic overloading and
copy semantics of inheritance. In this paper we present a core
object-oriented imperative language that integrates all these
features in a formal framework. We define a static type system and a
translation of the language into the meta-language λ_object,, in order
to account for semantic issues and prove type safety of our
proposal.
We extend the simply typed
λ-calculus with unbind and rebind primitive
constructs. That is, a value can be a fragment of open code,
which in order to be used should be explicitly rebound. This
mechanism nicely coexists with standard static binding. The
motivation is to provide an unifying foundation for mechanisms of
dynamic scoping, where the meaning of a name is
determined at runtime, rebinding, such as dynamic updating
of resources and exchange of mobile code, and delegation,
where an alternative...
We extend the simply typed
λ-calculus with unbind and rebind primitive
constructs. That is, a value can be a fragment of open code,
which in order to be used should be explicitly rebound. This
mechanism nicely coexists with standard static binding. The
motivation is to provide an unifying foundation for mechanisms of
dynamic scoping, where the meaning of a name is
determined at runtime, rebinding, such as dynamic updating
of resources and exchange of mobile code, and delegation,
where an alternative...
Monads have been employed in programming languages for modeling various language features, most importantly those that involve side effects. In particular, Haskell’s IO monad provides access to I/O operations and mutable variables, without compromising referential transparency. Cyclic definitions that involve monadic computations give rise to the concept of value-recursion, where the fixed-point computation takes place only over the values, without repeating or losing effects. In this paper, we...
Monads have been employed in programming languages for modeling
various language features, most importantly those that involve
side effects. In particular, Haskell's IO monad provides
access to I/O operations and mutable variables, without compromising
referential transparency. Cyclic definitions that involve monadic computations
give rise to the concept of value-recursion, where the fixed-point
computation takes place only over the values, without repeating or losing
effects. In this paper,...
This paper sketches the state of the art in the application of mechanical theorem provers to the verification of commercial computer hardware and software. While the paper focuses on the theorem proving system ACL2, developed by the two authors, it references much related work in formal methods. The paper is intended to satisfy the curiosity of readers interested in logic and artificial intelligence as to the role of mechanized theorem proving in hardware and software design today. In addition,...
The paradigm of type-based termination is explored for functional programming with recursive data types. The article introduces , a lambda-calculus with recursion, inductive types, subtyping and bounded quantification. Decorated type variables representing approximations of inductive types are used to track the size of function arguments and return values. The system is shown to be type safe and strongly normalizing. The main novelty is a bidirectional type checking algorithm whose soundness is...
Currently displaying 1 –
20 of
24