The search session has expired. Please query the service again.
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...
In this paper we argue that for fuzzy unification we need a procedural and declarative semantics (as opposed to the two valued case, where declarative semantics is hidden in the requirement that unified terms are syntactically – letter by letter – identical). We present an extension of the syntactic model of unification to allow near matches, defined using a similarity relation. We work in Hájek’s fuzzy logic in narrow sense. We base our semantics on a formal model of fuzzy logic programming extended...
This text includes the definition and basic notions of product of posets, chain-complete and flat posets, flattening operation, and the existence theorems of recursive call using the flattening operator. First part of the article, devoted to product and flat posets has a purely mathematical quality. Definition 3 allows to construct a flat poset from arbitrary non-empty set [12] in order to provide formal apparatus which eanbles to work with recursive calls within the Mizar langauge. To achieve 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...
This paper addresses an ongoing experience in the design of an artificial agent
taking decisions
and combining them with the decisions taken by human agents.
The context is a serious game research project,
aimed at computer-based support for participatory management of protected areas
(and more specifically national parks)
in order to promote biodiversity conservation and social inclusion.
Its objective is
to help various stakeholders (e.g., environmentalist, tourism operator)
to collectively understand...
The C++// language (pronounced C++ parallel) was designed and implemented with the aim of importing reusability into parallel and concurrent programming, in the framework of a mimd model. From a reduced set of rather simple primitives, comprehensive and versatile libraries are defined. In the absence of any syntactical extension, the C++// user writes standard C++ code. The libraries are themselves extensible by the final users, making C++// an open system. Two specific techniques to improve performances...
The C++// language (pronounced C++parallel)
was designed and implemented with the aim of importing
reusability into parallel and concurrent
programming, in the framework of a mimd model.
From a reduced set of rather simple primitives,
comprehensive and versatile libraries are defined.
In the absence of any syntactical extension,
the C++// user
writes standard C++ code.
The libraries are themselves
extensible by the final users, making C++// an open system. Two specific techniques to improve performances...
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.
Currently displaying 1 –
19 of
19