@comment{{Al final apareció en 2018}}
@comment{{2015}}
@inproceedings{susana:2007:robocup_IEEE,
tipoactividad = {Ponencias en congresos},
internacional = {yes},
author = {Mu{\~{n}}oz-Hern{\'{a}}ndez, Susana and Wiratna Sari Wiguna},
title = {Fuzzy Prolog as Cognitive Layer in RoboCupSoccer},
revisores = {yes},
descripcion = {},
booktitle = {IEEE Symposium on Computational Intelligence and Games (2007
IEEE Symposia Series in Computational Intelligence)},
pages = {340-345},
year = {2007},
series = {IEEE},
address = {Honolulu, Hawaii},
month = {April}
}
@inproceedings{susana:2007:robocup_IFSA,
tipoactividad = {Ponencias en congresos},
internacional = {yes},
author = {Mu{\~{n}}oz-Hern{\'{a}}ndez, Susana and Wiratna Sari Wiguna},
title = {Fuzzy Cognitive Layer in RoboCupSoccer},
revisores = {yes},
booktitle = {12th International Fuzzy Systems Association World Congress
(IFSA 2007). Foundations of Fuzzy Logic and Soft Computing},
pages = {635-645},
year = {2007},
optnumber = {4529},
optseries = {LNAI},
address = {Canc{\'u}n, M{\'e}xico},
month = {June},
publisher = {Springer}
}
@inproceedings{DBLP:conf/tlca/LiptonN07,
tipoactividad = {Ponencias en congresos},
internacional = {yes},
revisores = {yes},
author = {James Lipton and Susana Nieva},
title = {Higher-Order Logic Programming Languages with
Constraints: A Semantics},
booktitle = {Typed Lambda Calculi and Applications},
descripcion = {Definimos una sem{\'{a}}ntica tipo Kripke para un lenguaje
de programaci{\'{o}}n l{\'{o}}gica de orden superior con
restricciones, basado en la Teor{\'{i}}a de Tipos de
Church y un formalismo gen{\'{e}}rico de restricciones.},
pages = {272--289},
address = {Paris, France},
month = {June 26--28},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = 4583,
year = 2007,
isbn = {978-3-540-73227-3}
}
@article{pareja:marinno:2007:novatica:papiroflexia,
tipoactividad = {Art{\'{i}}culos en revistas},
internacional = {no},
author = {Crist{\'{o}}bal Pareja Flores and Julio Mari{\~{n}}o Carballo},
title = {Papiroflexia},
journal = {Nov{\'{a}}tica},
issn = {0211-2124},
year = 2007,
volume = 1,
number = 189,
pages = {73--75},
month = sep,
descripcion = {Contribuci{\'{o}}n semiperi{\'{o}}dica a la columna "Programar es Crear"
de la revista Nov{\'{a}}tica. En esta ocasi{\'{o}}n describimos la
soluci{\'{o}}n al problema E del Concurso de Programaci{\'{o}}n de la
Comunidad de Madrid del a{\~{n}}o 2006.}
}
@techreport{xmc:2007:_study_of_exist_codin_rule,
tipoactividad = {Otras publicaciones},
internacional = {yes},
author = {Julio Mari{\~{n}}o and {{\'{A}}ngel} Herranz and Lars-{\AA}ke Fredlund and
Manuel Carro and Pablos-Ceruelo, V{\'{i}}ctor and Guillem Marpons and Juan
Jos{\'{e}} {Moreno-Navarro}},
title = {Study of existing coding rule formalisms and compendium of
common hazards. {U}se of Coding Rules in Software Industry},
descripcion = {Estudio de los formalismos existentes para reglas de
codificaci{\'{o}}n, relaci{\'{o}}n de riesgos de software m{\'{a}}s comunes y
resultados de encuesta a socios del proyecto {GlobalGCC}.},
institution = {Facultad de Inform{\'{a}}tica, Universidad Polit{\'{e}}cnica de Madrid},
year = 2007,
address = {Boadilla del Monte, Madrid, Spain},
month = nov,
annote = {Deliverable for the {GlobalGCC} Project}
}
@inproceedings{marpons:2007:wlpe,
tipoactividad = {Ponencias en congresos},
internacional = {yes},
author = {Guillem Marpons and Julio Mari{\~n}o and {{\'{A}}ngel}
Herranz and Lars-{\AA}ke Fredlund and Manuel Carro and Juan
Jos{\'e} {Moreno-Navarro}},
title = {Automatic Coding Rule Conformance Checking Using Logic
Programs},
abstract = { Coding rules are customarily used to constrain the use (or
abuse) of certain constructions in a programming language.
Standard coding rule sets exist that target different
languages and application domains. However, these rules are
usually written using a natural language, which is
intrinsically ambiguous, and which may hinder their
automatic application. This short paper presents some early
work aiming at defining a framework to formalise and check
for coding rule conformance using logic programming. We
show how a certain class of rules -- \emph{structural} rules
-- can be reformulated as logic programs. Some real
examples, including Prolog code formalising them, are shown
and discussed. },
revisores = {yes},
booktitle = {17th Workshop on Logic-based methods in Programming
Environments, {WLPE} 2007},
pages = 47,
url = {http://arxiv.org/abs/0711.0344},
year = 2007,
editor = {Patricia Hill and Vim Vanhoof},
address = {Porto, Portugal},
month = sep
}
@article{marpons:2007:corr,
author = {Guillem Marpons and Julio Mari{\~n}o and {{\'{A}}ngel}
Herranz and Lars-{\AA}ke Fredlund and Manuel Carro and Juan
Jos{\'e} {Moreno-Navarro}},
abstract = { Coding rules are customarily used to constrain the use (or
abuse) of certain constructions in a programming language.
Standard coding rule sets exist that target different
languages and application domains. However, these rules are
usually written using a natural language, which is
intrinsically ambiguous, and which may hinder their
automatic application. This short paper presents some early
work aiming at defining a framework to formalise and check
for coding rule conformance using logic programming. We
show how a certain class of rules -- \emph{structural} rules
-- can be reformulated as logic programs. Some real
examples, including Prolog code formalising them, are shown
and discussed. },
title = {Automatic Coding Rule Conformance Checking Using Logic
Programs},
journal = {CoRR},
volume = {abs/0711.0344},
year = 2007,
month = nov,
url = {http://arxiv.org/abs/0711.0344},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@misc{marpons:2007:sas,
tipoactividad = {Otras publicaciones},
internacional = {yes},
abstract = { This short paper presents some early work in the context of
an European project aiming at defining a framework to
formalise and check for coding rule conformance using logic
programming. We show how a certain class of rules --
\emph{structural} rules -- can be reformulated as logic
programs. This provides both a framework for formal
specification and also for automatic conformance checking
using a Prolog engine. },
revisores = {yes},
author = {Guillem Marpons and Julio Mari{\~{n}}o and {{\'{A}}ngel} Herranz and
Lars-{\AA}ke Fredlund and Manuel Carro and Juan Jos{\'{e}}
{Moreno-Navarro}},
title = {Towards Checking Coding Rule Conformance Using Logic
Programming},
month = aug,
year = 2007,
note = {Poster at the 14th International Static Analysis
Symposium, SAS 2007},
address = {Kongens Lyngby, Denmark},
pdf = {http://babel.ls.fi.upm.es/~gmarpons/pubs/SAS07CodingrulesPoster.pdf}
}
@unpublished{garcia:2007:acsd,
tipoactividad = {Ponencias en congresos},
internacional = {yes},
author = {{{\'{A}}lvaro} {Garc{\'{i}}a-P{\'{e}}rez} and Nelson {Medinilla Mart{\'{i}}nez}},
title = {The Ambiguity Criterion in Software Design},
url = {http://se.cs.toronto.edu/IWLU/program.html},
note = {International Workshop on Living with Uncertainties 2007
(IWLU'07), Co-located with the 22nd International conference
on Automated Software engineering (ASE'07)},
month = nov,
year = {2007}
}
@article{gabbay:frelog,
tipoactividad = {Art{\'{i}}culos en revistas},
internacional = {yes},
author = {Murdoch J. Gabbay},
title = {Fresh Logic: proof-theory and semantics for FM and nominal
techniques},
journal = {Journal of Applied Logic},
year = {2007},
url = {http://www.gabbay.org.uk/papers/frelog.pdf},
optdescripcion = {},
optissn = {},
optkey = {},
volume = {5},
number = {2},
pages = {356-387},
optmonth = {},
optnote = {},
optannote = {},
abstract = {In this paper we introduce Fresh Logic, a natural deduction
style first-order logic extended with term-formers and
quantifiers derived from the FM-sets model of names and
binding in abstract syntax. Fresh Logic can be classical or
intuitionistic depending on whether we include a law of
excluded middle; we present a proof-normalisation procedure
for the intuitionistic case and a semantics based on Kripke
models in FM-sets for which it is sound and complete.}
}
@article{gabbay:genmn,
tipoactividad = {Art{\'{i}}culos en revistas},
internacional = {yes},
author = {Murdoch J. Gabbay},
title = {A general mathematics of names},
journal = {Information and Computation},
year = {2007},
optdescripcion = {},
optissn = {},
optkey = {},
volume = {205},
number = {7},
pages = {982-1011},
optmonth = {},
optnote = {},
optannote = {},
url = {http://www.gabbay.org.uk/papers/genmn.pdf},
abstract = {We introduce FMG (Fraenkel-Mostowski Generalised) set
theory, a generalisation of FM set theory which allows
binding of infinitely many names instead of just finitely
many names. We apply this generalisation to show how three
presentations of syntax--de Bruijn indices, FM sets, and
name-carrying syntax--have a relation generalising to all
sets and not only sets of syntax trees. We also give
syntax-free accounts of Barendregt representatives, scope
extrusion, and other phenomena associated to
$\alpha$-equivalence. Our presentation uses a novel
presentation based not on a theory but on a concrete model
U.}
}
@article{gabbay:nomr-jv,
tipoactividad = {Art{\'{i}}culos en revistas},
internacional = {yes},
author = {Maribel Fern\'{a}ndez and Murdoch J. Gabbay},
title = {Nominal Rewriting (journal version)},
journal = {Information and Computation},
year = {2007},
optdescripcion = {},
optissn = {},
optkey = {},
volume = {205},
number = {6},
pages = {917-965},
optmonth = {},
optnote = {},
optannote = {},
url = {http://www.gabbay.org.uk/papers/nomr-jv.pdf},
abstract = {Nominal rewriting is based on the observation that if we add
support for $\alpha$-equivalence to first-order syntax using
the nominal-set approach, then systems with binding,
including higher-order reduction schemes such as
$\lambda$-calculus beta-reduction, can be smoothly
represented. Nominal rewriting maintains a strict
distinction between variables of the object-language (atoms)
and of the meta-language (variables or unknowns). Atoms may
be bound by a special abstraction operation, but variables
cannot be bound, giving the framework a pronounced
first-order character, since substitution of terms for
variables is not capture-avoiding. We show how good
properties of first-order rewriting survive the extension,
by giving an efficient rewriting algorithm, a critical pair
lemma, and a confluence theorem for orthogonal systems.}
}
@article{gabbay:hientt,
tipoactividad = {Art{\'{i}}culos en revistas},
internacional = {yes},
author = {Murdoch J. Gabbay},
title = {Hierarchical Nominal Terms and their Theory of
Rewriting},
journal = {Electronic Notes in Theoretical Computer Science},
year = 2007,
issn = {1571-0661},
volume = 174,
number = 5,
pages = {37-52},
url = {http://www.gabbay.org.uk/papers/hientt.pdf},
abstract = {Nominal rewriting introduced a novel method of
specifying rewriting on syntax-with-binding. We
extend this treatment of rewriting with hierarchy of
variables representing increasingly 'meta-level'
variables, e.g. in hierarchical nominal term
rewriting the meta-level unknowns (representing
unknown terms) in a rewrite rule can be 'folded
into' the syntax itself (and rewritten). To the
extent that rewriting is a mathematical
meta-framework for logic and computation, and
nominal rewriting is a framework with native support
for binders, hierarchical nominal term rewriting is
a meta-to-the-omega level framework for logic and
computation with binders.}
}
@inproceedings{gabbay:forcie,
tipoactividad = {Ponencias en congresos},
internacional = {yes},
author = {Murdoch J. Gabbay and Aad Mathijssen},
title = {A Formal Calculus for Informal Equality with Binding},
optrevisores = {},
optdescripcion = {},
optisbn = {},
optcrossref = {},
optkey = {},
booktitle = {Proceedings of WOLLIC'07},
pages = {162-176},
year = {2007},
opteditor = {},
volume = {4576},
optnumber = {},
series = {Lecture Notes in Computer Science},
address = {},
optmonth = {},
optorganization = {},
optpublisher = {},
optnote = {},
optannote = {},
url = {http://www.gabbay.org.uk/papers/forcie.pdf},
abstract = {In informal mathematical usage we often reason using
languages with binding. We usually find ourselves placing
capture-avoidance constraints on where variables can and
cannot occur free. We describe a logical derivation system
which allows a direct formalisation of such assertions,
along with a direct formalisation of their constraints. We
base our logic on equality, probably the simplest available
judgement form. In spite of this, we can axiomatise systems
of logic and computation such as first-order logic or the
lambda-calculus in a very direct and natural way. We
investigate the theory of derivations, prove a suitable
semantics sound and complete, and discuss existing and
future research.}
}
@inbook{hemo:2007:mrdps,
author = {{{\'{A}}ngel} Herranz and Juan Jos{\'{e}} {Moreno-Navarro}},
title = {Design Pattern Formalization Techniques},
chapter = {Modeling and Reasoning about Design Patterns in
{SLAM-SL}},
publisher = {IGI Publishing},
year = {2007},
month = mar,
isbn = {978-1-59904-219-0},
note = {Other ISBN: 978-1-59904-221-3},
abstract = {The main main subject of the chapter is how design
patterns can be described as class
operations. Additionally, we describe two possible
applications: how to reason about design patterns,
and how a design can be automatically refactored
using design patterns.},
tipoactividad = {Cap{\'{i}}tulos de libro},
internacional = {yes},
description = {El principal objetivo del cap{\'{i}}tulo es el estudio de
la descripci{\'{o}}n de patrones de dise{\~{n}}o como operadores
matem{\'{a}}ticos sobre clases. Adem{\'{a}}s, se describen dos
posibles aplicaciones de la formalizaci{\'{o}}n:
razonamiento sobre patrones de dise{\~{n}}o y la
refactorizaci{\'{o}}n autom{\'{a}}tica de los dise{\~{n}}os utilizando
los operadores de clases definidos.},
pdf = {http://babel.ls.fi.upm.es/~angel/papers/taibichapter-finalcopy.pdf}
}
@article{mahemo:2007:dapp,
tipoactividad = {Art{\'{i}}culos en revistas},
internacional = {yes},
author = {Julio Mari{\~{n}}o and {{\'{A}}ngel} Herranz and Juan Jos{\'{e}}
{Moreno-Navarro}},
title = {Demand Analysis with Partial Predicates},
journal = {Theory and Practice of Logic Programming},
issn = {1471-0684},
year = 2007,
volume = 7,
number = {1-2},
pages = {153-182},
month = jan,
descripcion = {El an{\'{a}}lisis de demanda pretende determinar en tiempo de
compilaci{\'{o}}n qu{\'{e}} c{\'{a}}lculos van a ser realmente utilizados
durante la ejecuci{\'{o}}n de un programa. Esta informaci{\'{o}}n puede
ser muy relevante para la implementaci{\'{o}}n de lenguajes
l{\'{o}}gico-funcionales. Este trabajo propone un marco sem{\'{a}}ntico
de predicados parciales, que podr{\'{i}}amos ver como
realizaciones constructivas de ideales sobre un cierto
dominio. Con esto conseguimos dar una presentaci{\'{o}}n concisa y
unificada de una familia de an{\'{a}}lisis de demanda,
relacionarlo con otras propuestas, ideas para su
implementaci{\'{o}}n y, finalmente, demostrar la correcci{\'{o}}n de una
propuesta anterior basada en la resoluci{\'{o}}n de ecuaciones de
demanda.}
}
@article{DBLP:journals/entcs/AriasMP07,
author = {Emilio Jes{\'u}s {Gallego Arias} and Julio
{Mari{\~n}o-Carballo} and Jos{\'e} Mar\'{\i}a {Rey Poza}},
title = {A Proposal for Disequality Constraints in Curry},
journal = {Electr. Notes Theor. Comput. Sci.},
volume = {177},
year = {2007},
pages = {269-285},
issn = {1571-0661},
ee = {http://dx.doi.org/10.1016/j.entcs.2007.01.014},
abstract = {We describe the introduction of disequality constraints over
algebraic data terms in the functional logic language Curry,
and their implementation in Sloth, our Curry compiler. This
addition extends the standard definition of Curry in several
ways. On one hand, we provide a disequality counterpart to
the constraint equality operator (=:=). Secondly, boolean
equality operators are also redefined to cope with
constructive disequality information, which leads to a more
symmetric design w.r.t. the existing one. Semantically
speaking, our implementation is very similar to previous
proposals, although there are some novel aspects. One of
them is that the implementation is partly based on an
existing finite domain (FD) constraint solver, which
provides a more efficient execution in some examples and,
more important, the first complete implementation of
disequality constraints over finite types. A detailed
description of the finite type case is provided, including:
(i) the use of the FD solver; (ii) an algorithm for analysing
cardinality of types, and (iii) how to deal with cardinality
information at run time. Some benchmarks, an operational
semantics minimally extending the one in the Curry draft,
and a moderately detailed description of the implementation
complete the paper.},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{Genericsem,
tipoactividad = {Ponencias en congresos},
internacional = {yes},
revisores = {yes},
author = {Emilio Jes{\'u}s {Gallego Arias} and Julio
{Mari{\~n}o-Carballo} and Jos{\'e} Mar\'{\i}a {Rey Poza}},
title = {A Generic Semantics for Constraint Functional Logic
Programming},
booktitle = {Proc.\ of the 16th Int'l Workshop on Functional and
(Constraint) Logic Programming (WFLP 2007)},
descripcion = {Proponemos una sem{\'{a}}ntica operacional para programas l{\'{o}}gico
funcionales perezosos con restricciones que es gen{\'{e}}rica en
tanto que permite la integraci{\'{o}}n de diferentes resolvedores
de restricciones en un n{\'{u}}cleo com{\'{u}}n de una manera bastante
limpia. El dise{\~{n}}o de esta sem{\'{a}}ntica trata de satisfacer dos
principios aparentemente contradictorios: la necesidad de
dar soporte a la evaluaci{\'{o}}n perezosa desde el resolvedor de
restricciones y el principio de caja negra aplicado al
dise{\~{n}}o de la relaci{\'{o}}n entre el resolvedor y el motor de
inferencia.},
year = 2007,
month = {June 25},
address = {Paris, France}
}
@mastersthesis{Relunif,
author = {Emilio Jes{\'u}s {Gallego Arias}},
title = {Relational Unification},
school = {Facultad de Inform{\'{a}}tica, Universidad Polit{\'{e}}cnica de Madrid},
year = 2007,
month = oct,
note = {Advisor: James Lipton}
}
@inproceedings{pni:tfp07:adtfunctor:proceedings,
tipoactividad = {Ponencias en congresos},
internacional = {yes},
revisores = {yes},
author = {Pablo Nogueira},
title = {When is an Abstract Data Type a Functor?},
booktitle = {Proceedings of the 7th {S}ymposium on {T}rends in {F}unctional
{P}rogramming - {TFP}'06},
pages = {217-231},
optpublisher = {left out on purpose},
year = 2007,
month = {April 19-21},
address = {Nottingham, UK},
editor = {Henrik Nilsson},
note = {Winner of Best Student Paper Award},
abstract = {A parametric algebraic data type is a functor when we can
apply a function to its data components while satisfying
certain equations. We investigate whether parametric
abstract data types can be functors. We provide a general
definition for their map operation that needs only satisfy
one equation. The definability of this map depends on
properties of interfaces and is a sufficient condition for
functoriality. Instances of the definition for particular
abstract types can then be constructed using their axiomatic
semantics. The definition and the equation can be adapted to
determine, necessarily and sufficiently, whether an ADT is a
functor for a given implementation},
pdf = {http://babel.ls.fi.upm.es/~pablo/Papers/adt-functors.pdf}
}
@incollection{pni:tfp07:adtfunctor:chapter,
tipoactividad = {Cap{\'{i}}tulos de libros},
internacional = {yes},
author = {Pablo Nogueira},
title = {When is an Abstract Data Type a Functor?},
booktitle = {Trends in Functional Programming},
isbn = {978-1-84150-188-8},
pages = {217-231},
publisher = {Intellect},
year = 2007,
month = {September 30},
editor = {Henrik Nilsson},
volume = 7,
chapter = 13,
note = {Winner of Best Student Paper Award},
abstract = {A parametric algebraic data type is a functor when we can
apply a function to its data components while satisfying
certain equations. We investigate whether parametric
abstract data types can be functors. We provide a general
definition for their map operation that needs only satisfy
one equation. The definability of this map depends on
properties of interfaces and is a sufficient condition for
functoriality. Instances of the definition for particular
abstract types can then be constructed using their axiomatic
semantics. The definition and the equation can be adapted to
determine, necessarily and sufficiently, whether an ADT is a
functor for a given implementation},
pdf = {http://babel.ls.fi.upm.es/~pablo/Papers/adt-functors.pdf}
}
@article{fredlund_svensson:mcErlangSIGPLAN,
tipoactividad = {Art{\'{i}}culos en revistas},
internacional = {yes},
author = {Lars-{\AA}ke Fredlund and H. Svensson},
title = {Mc{E}rlang: a model checker for a distributed
functional programming language},
revisores = {yes},
journal = {ACM SIGPLAN Notices},
issn = {0362-1340},
year = 2007,
abstract = {We present a model checker for verifying distributed
programs written in the Erlang programming
language. Providing a model checker for Erlang is
especially rewarding since the language is by now
being seen as a very capable platform for developing
industrial strength distributed applications with
excellent failure tolerance characteristics. In
contrast to most other Erlang verification attempts,
we provide support for a very substantial part of
the language. The model checker has full Erlang data
type support, support for general process
communication, node semantics (inter-process behave
subtly different from intra-process communication),
fault detection and fault tolerance through process
linking, and can verify programs written using the
OTP Erlang component library (used by most modern
Erlang programs). As the model checking tool is
itself implemented in Erlang we benefit from the
advantages that a (dynamically typed) functional
programming language offers: easy prototyping and
experimentation with new verification algorithms,
rich executable models that use complex data
structures directly programmed in Erlang, the
ability to treat executable models interchangeably
as programs (to be executed directly by the Erlang
interpreter) and data, and not least the possibility
to cleanly structure and to cleanly combine various
verification sub-tasks. In the paper we discuss the
design of the tool and provide early indications on
its performance.},
volume = 42,
number = 9,
pages = {125-136}
}
@inproceedings{fredlund_svensson:mcErlangICFP,
tipoactividad = {Ponencias en congresos},
internacional = {yes},
revisores = {yes},
author = {Lars-{\AA}ke Fredlund and H. Svensson},
title = {Mc{E}rlang: a model checker for a distributed
functional programming language},
booktitle = {Proceedings of the 12th ACM SIGPLAN International
conference on functional programming (ICFP 2007)},
abstract = {We present a model checker for verifying distributed
programs written in the Erlang programming
language. Providing a model checker for Erlang is
especially rewarding since the language is by now
being seen as a very capable platform for developing
industrial strength distributed applications with
excellent failure tolerance characteristics. In
contrast to most other Erlang verification attempts,
we provide support for a very substantial part of
the language. The model checker has full Erlang data
type support, support for general process
communication, node semantics (inter-process behave
subtly different from intra-process communication),
fault detection and fault tolerance through process
linking, and can verify programs written using the
OTP Erlang component library (used by most modern
Erlang programs). As the model checking tool is
itself implemented in Erlang we benefit from the
advantages that a (dynamically typed) functional
programming language offers: easy prototyping and
experimentation with new verification algorithms,
rich executable models that use complex data
structures directly programmed in Erlang, the
ability to treat executable models interchangeably
as programs (to be executed directly by the Erlang
interpreter) and data, and not least the possibility
to cleanly structure and to cleanly combine various
verification sub-tasks. In the paper we discuss the
design of the tool and provide early indications on
its performance.},
isbn = {978-1-59593-815-2},
year = 2007,
month = oct
}
@inproceedings{svensson_fredlund:accsem,
tipoactividad = {Ponencias en congresos},
internacional = {yes},
revisores = {yes},
author = {H. Svensson and Lars-{\AA}ke Fredlund},
title = {A more accurate semantics for distributed {E}rlang},
booktitle = {Proceedings of the 2007 ACM SIGPLAN Erlang Workshop},
abstract = {In order to formally reason about distributed Erlang
systems, it is necessary to have a formal semantics.
In a previous paper we have proposed such a
semantics for distributed Erlang. However, recent
work with a model checker for Erlang revealed that
the previous attempt was not good enough. In this
paper we present a more accurate semantics includes
several modifications and additions to the semantics
for distributed Erlang proposed by Claesson and
Svensson in 2005, which in turn is an extension to
Fredlund's formal single-node semantics for
Erlang. The most distinct addition to the previous
semantics is the possibility to correctly model
disconnected nodes.},
year = 2007,
isbn = {978-1-59593-675-2},
month = oct
}
@inproceedings{svensson_fredlund:pitfalls,
tipoactividad = {Ponencias en congresos},
internacional = {yes},
revisores = {yes},
author = {H. Svensson and Lars-{\AA}ke Fredlund},
year = 2007,
isbn = {978-1-59593-675-2},
month = oct,
abstract = {We investigate the distributed part of the Erlang
programming language, with an aim to develop robust
distributed systems and algorithms running on top of
Erlang runtime systems. Although the step to convert
an application running on a single node to a fully
distributed (multi-node) application is deceptively
simple (changing calls to \texttt{spawn} so that
processes are spawned on different nodes), there are
some corner cases in the Erlang language and API
where the introduction of distribution can cause
problems. In this paper we discuss a number of such
pitfalls, where the semantics of communicating
processes differs significantly depending if the
processes reside on the same node or not, we also
provide some guidelines for safe programming of
distributed systems.},
title = {Programming distributed {E}rlang applications:
pitfalls and recipes},
booktitle = {Proceedings of the 2007 ACM SIGPLAN Erlang Workshop}
}
@inproceedings{fredlund_penas:mcErlangVodka,
tipoactividad = {Ponencias en congresos},
internacional = {yes},
revisores = {yes},
isbn = {978-3-540-75866-2},
author = {Lars-{\AA}ke Fredlund and J. {S{\'{a}}nchez Penas}},
title = {Model checking a video-on-demand server using
Mc{E}rlang},
booktitle = {Proceedings of the 11th International Conference on
Computer Aided Systems Theory (Eurocast 2007)},
abstract = {The article describes a method to obtain performance
measurements from complex distributed systems using
a model checking approach. We illustrate the
approach by applying it to a video-on-demand
application developed in Erlang. To obtain
performance measurements concerning e.g.\ streaming
capacity, and identify system bottlenecks, we used
the McErlang model checker which implements a large
part of the Erlang API. Answers to capacity queries
are computed as measures over paths in the system
state graph, and the combination of an on-the-fly
model checker (not requiring the generation of the
complete state graph) with a powerful language
(Erlang itself) for expressing correctness claims,
made it possible to analyse substantially sized
systems.},
volume = 4739,
series = {LNCS},
publisher = {Springer},
year = 2007,
month = feb
}
@proceedings{fredlund_thompson:Erlang07,
tipoactividad = {Libros},
internacional = {yes},
editor = {S. Thompson and Lars-{\AA}ke Fredlund},
booktitle = {Proceedings of the 2007 ACM SIGPLAN Erlang Workshop},
title = {Proceedings of the 2007 ACM SIGPLAN Erlang Workshop},
year = 2007,
month = oct,
abstract = {Proceedings of the 2007 ACM SIGPLAN Erlang Workshop.},
editorial = {ACM Press},
isbn = {978-1-59593-675-2}
}
This file was generated by bibtex2html 1.98.