Page 1

Displaying 1 – 19 of 19

Showing per page

Deciding inclusion of set constants over infinite non-strict data structures

Manfred Schmidt-Schauss, David Sabel, Marko Schütz (2007)

RAIRO - Theoretical Informatics and Applications

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...

Declarative and procedural semantics of fuzzy similarity based unification

Peter Vojtáš (2000)

Kybernetika

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...

Definition of Flat Poset and Existence Theorems for Recursive Call

Kazuhisa Ishida, Yasunari Shidama, Adam Grabowski (2014)

Formalized Mathematics

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...

Denotational aspects of untyped normalization by evaluation

Andrzej Filinski, Henning Korsholm Rohde (2005)

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications

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,...

Denotational aspects of untyped normalization by evaluation

Andrzej Filinski, Henning Korsholm Rohde (2010)

RAIRO - Theoretical Informatics and Applications

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...

Design of a Participatory Decision Making Agent Architecture Based on Argumentation and Influence Function – Application to a Serious Game about Biodiversity Conservation

Alessandro Sordoni, Jean-Pierre Briot, Isabelle Alvarez, Eurico Vasconcelos, Marta de Azevedo Irving, Gustavo Melo (2010)

RAIRO - Operations Research

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...

Distributed objects for parallel numerical applications

Francoise Baude, Denis Caromel, David Sagnol (2002)

ESAIM: Mathematical Modelling and Numerical Analysis - Modélisation Mathématique et Analyse Numérique

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...

Distributed Objects for Parallel Numerical Applications

Francoise Baude, Denis Caromel, David Sagnol (2010)

ESAIM: Mathematical Modelling and Numerical Analysis

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...

Domain-Free λµ-Calculus

Ken-Etsu Fujita (2010)

RAIRO - Theoretical Informatics and Applications

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,...

Dynamic overloading with copy semantics in object-oriented languages: a formal account

Lorenzo Bettini, Sara Capecchi, Betti Venneri (2009)

RAIRO - Theoretical Informatics and Applications

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

Page 1