[GM09b]
Murdoch J. Gabbay and Aad Mathijssen. Nominal universal algebra: equational logic with names and binding. Journal of Logic and Computation, 19(6):1455--1508, December 2009. [ bib | DOI ]
[GL09]
Murdoch J. Gabbay and Stéphane Lengrand. The lambda-context calculus (extended version). Information and Computation, 207:1369--1400, December 2009. [ bib | DOI ]
[Gar09a]
Álvaro García-Pérez. Evaluation of the λ-calculus. generic evaluators. Talk at the Algebra of Programming Group meeting, October 23 2009. [ bib | http ]
[PC09a]
Víctor Pablos-Ceruelo. Negative non-ground queries in well founded semantics. Master's thesis, Faculdade de Ciências e Tecnologia da Universidade Nova de Lisboa, October 2009. Advisor: José Júlio Alves Alferes, Calificación: Notable. [ bib | .html | .pdf ]
[CRVP09]
Oscar Corcho, Catherine Roussey, Luis Manuel Vilches Blázquez, and Iván Pérez. Pattern-based OWL Ontology Debugging Guidelines. In Eva Blomqvist, Kurt Sandkuhl, Francois Scharffe, and Vojtech Svatek., editors, Workshop on Ontology Patterns (WOP 2009), collocated with the 8th International Semantic Web Conference (ISWC-2009)., CEUR Workshop proceedings, pages 68--82, October 2009. http://sunsite.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-516/. [ bib | http ]
Debugging inconsistent OWL ontologies is a tedious and time-consuming task where a combination of ontology engineers and domain experts is often required to understand whether the changes to be performed are actually dealing with formalisation errors or changing the intended meaning of the original knowledge model. Debugging services from existing ontology engineering tools and debugging strategies available in the literature aid in this task. However, in complex cases they are still far from providing adequate support to ontology developers, due to their lack of eciency or precision when explaining the main causes for unsatisfiable classes, together with little support for proposing solutions for them. We claim that it is possible to provide additional support to ontology developers, based on the identification of common antipatterns and a debugging strategy, which can be combined with the use of existing tools in order to make this task more effective.

[PC09b]
Iván Pérez and Oscar Corcho. Pattern Definitions and Semantically Annotated Instances. In Eva Blomqvist, Kurt Sandkuhl, Francois Scharffe, and Vojtech Svatek, editors, Workshop on Ontology Patterns (WOP 2009), collocated with the 8th International Semantic Web Conference (ISWC-2009), CEUR Workshop proceedings, pages 131--138, October 2009. [ bib | http ]
Ontology design patterns are normally instantiated by replicating and adapting the pattern concepts and roles. The relation between pattern definitions and their instantiations is documented in natural language. The use of parametric ontologies or pattern-reuse modifications to OWL-DL has been suggested before, but so far only practical aspects have been analysed, leaving the formal semantics of these extensions as future work. In this work we present formal definitions for ontology pattern and pattern instantiations, together with the semantics of instantiation. We propose the use of semantic annotations to describe and generate OWL pattern instantiations, without the need for explicit ontology replication, and provide tools to support this process.

[BF09b]
Clara Benac Earle and Lars-Åke Fredlund. Rigorous software development using mcerlang. In 14th Conference on Software Engineering and Databases, JISBD'09, pages 335--338, San Sebastián, Spain, September 8--11 2009. [ bib ]
[San09]
Rahmat Bagas Santoso. Distributed osgi: service and semantic exposition. Master's thesis, Facultad de Informática, Universidad Politécnica de Madrid, September 2009. Advisor: Lars-Ake Fredlund, Calificación: Sobresaliente cum laude. [ bib ]
[Pér09]
Iván Pérez. Gadget composition and automatic discovery in EzWeb. Master's thesis, Facultad de Informática, Universidad Politécnica de Madrid, September 2009. Advisor: Susana Muñoz-Hernández, Calificación: Notable. [ bib ]
[TB09]
S. Thompson and Clara Benac Earle, editors. Proceedings of the 2009 ACM SIGPLAN Erlang Workshop, September 2009. [ bib ]
Proceedings of the 2009 ACM SIGPLAN Erlang Workshop.

[Gar09b]
Álvaro García-Pérez. Exploring the β-hypercube. Master's thesis, Facultad de Informática, Universidad Politécnica de Madrid, September 2009. Advisor: Pablo Nogueira. [ bib ]
[MMC+09]
Guillem Marpons, Julio Mariño, Manuel Carro, Ángel Herranz, Lars-Åke Fredlund, Juan José Moreno-Navarro, and Álvaro Polo. A coding rule conformance checker integrated into GCC. ENTCS, 248:149--159, August 5 2009. [ bib | http ]
Coding rules are often used in industry to foster best practices when coding software and to avoid the many hazardous constructions present in languages such as C or C++. Predictable, reliable tools are needed to automatically measure adherence to these practices, as manually checking for compliance is cumbersome. Moreover, due to the wide range of possible coding rule sets, easy of customization is a need in order for these tools to be of practical use. With this aim in mind, we present an extension of the GNU Compiler Collection (GCC) that flags those code fragments that do not conform to coding rules belonging to a given set. These sets of coding rules can be defined using a high-level declarative language based on logic programming, thereby making it possible to easily check code for conformance with respect to rules addressing the particular needs of a project, company, or application area.

[GG09a]
Michael Gabbay and Murdoch J. Gabbay. Term sequent logic. In Proceedings of the 17th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2008), volume 246 of Electronic Notes in Theoretical Computer Science, pages 87--106, August 2009. [ bib | DOI ]
[GM09d]
Murdoch J. Gabbay and Dominic P. Mulligan. Two-level lambda-calculus. In Proceedings of the 17th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2008), volume 246, pages 107--129, August 2009. [ bib | DOI ]
[Gar09d]
Álvaro García-Pérez. A functional correspondence between parametric evaluators and which abstract machines? Talk at the Algebra of Programming Group meeting, June 6 2009. [ bib | .pdf ]
[MHM09a]
Susana Muñoz-Hernández and Jesús Martínez-Mateo. An opportunity for libre software companies: Emerging market in developing countries. The European Journal for the Informatics Professional, X(3):51--53, June 2009. [ bib ]
[PCSMH09]
Víctor Pablos-Ceruelo, Hannes Strass, and Susana Muñoz-Hernández. Rfuzzy---a framework for multi-adjoint fuzzy logic programming. In Fuzzy Information Processing Society, 2009. NAFIPS 2009. Annual Meeting of the North American Fuzzy Information Processing Society Annual Conference, pages 1--6, Cincinnati, Ohio, USA, June 2009. [ bib | DOI | http ]
Fuzzy Logic Programming aims at combining the advantages of Logic Programming (such as readability, conciseness, and a formally well-defined semantics) with the advantages of Fuzzy Logic (representability of imprecise and uncertain knowledge).

[Gar09c]
Álvaro García-Pérez. A functional approach to the observer pattern. Talk at the Algebra of Programming Group meeting, May 29 2009. [ bib | .pdf ]
[MHM09b]
Susana Muñoz-Hernández and Jesús Martínez-Mateo. Una oportunidad para las empresas de software libre: mercado emergente en los paises en vías de desarrollo. Novática, 1(199):44--46, May-June 2009. [ bib ]
[MMMPR09]
Jesús Martínez-Mateo, Susana Muñoz-Hernández, and David Pérez-Rey. c&d-learning Implementation Architecture: Adapting e-learning to Developing Countries. In First International Conference on Computer Supported Education (CSEDU), volume 1, pages 89--96, March 2009. [ bib ]
[THM09]
Toufik Taibi, Ángel Herranz, and Juan José Moreno-Navarro. Stepwise refinement validation of design patterns formalized in TLA+ using the TLC model checker. Journal of Object Technology (JOT, http://www.jot.fm/general/about/), 8(2):137--161, March 2009. [ bib | DOI | .pdf ]
Despite being around for only a little more than a decade, design patterns have proved to be successful reuse artifacts. However, the fact that they are mostly described informally gives rise to ambiguity and hinders correct usage. This paper discusses how to formally specify the "solution element" of patterns using TLA+, the formal specification language of Temporal Logic of Actions (TLA). The focus is first on formally specifying the most abstract version of a pattern before validly doing stepwise refinements by adding more details along the way until reaching a concrete implementation. Checking that the refinement properties hold was done using TLC (the TLA+ model checker).

[SMHPC09a]
Hannes Strass, Susana Muñoz-Hernández, and Víctor Pablos-Ceruelo. Multi-adjoint fuzzy logic programming with defaults and constructive answers. (unpublished), 2009. [ bib | .pdf ]
[Gab09a]
Murdoch J. Gabbay. Nominal algebra and the HSP theorem. Journal of Logic and Computation, 19(2):341--367, 2009. [ bib ]
[Gab09b]
Murdoch J. Gabbay. A study of substitution, using nominal techniques and Fraenkel-Mostowski sets. Theoretical Computer Science, 410(12-13):1159--1189, 2009. [ bib | DOI ]
[GM09c]
Murdoch J. Gabbay and Dominic Mulligan. Universal algebra over lambda-terms and nominal terms: the connection in logic between nominal techniques and higher-order variables. In ACM International Conference Proceeding Series, Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'09), pages 64--73, 2009. [ bib | DOI ]
[GM09a]
Murdoch J. Gabbay and Aad Mathijssen. A nominal axiomatisation of the lambda-calculus. Journal of Logic and Computation, 2009. Advance access (published online September 2009). [ bib | DOI ]
[DGM09]
Gilles Dowek, Murdoch J. Gabbay, and Dominic P. Mulligan. Permissive nominal terms and their unification. In Proceedings of the 24th Italian Conference on Computational Logic (CILC'09), 2009. [ bib ]
[EF09]
Clara Benac Earle and Lars-Åke Fredlund. Debugging and verification of multi-agent systems. In Roberto Moreno-Díaz, Franz Pichler, and Alexis Quesada-Arencibia, editors, Computer Aided Systems Theory - EUROCAST 2009, 12th International Conference, Las Palmas de Gran Canaria, Spain, February 15-20, 2009, Revised Selected Papers, volume 5717 of Lecture Notes in Computer Science, pages 263--270. Springer, 2009. [ bib | http ]
[SMHPC09b]
Hannes Strass, Susana Muñoz-Hernández, and Víctor Pablos-Ceruelo. Operational semantics for a fuzzy logic programming system with defaults and constructive answers. In João Paulo Carvalho, Didier Dubois, Uzay Kaymak, and João Miguel da Costa Sousa, editors, IFSA/EUSFLAT Conf., pages 1827--1832, 2009. [ bib | .pdf ]
[BF09a]
Clara Benac Earle and Lars-Åke Fredlund. Recent improvements to the mcerlang model checker. In Thompson and Benac Earle [TB09], pages 93--100. [ bib | http ]
In this paper we describe a number of recent improvements to the McErlang model checker, including a new source to source translation to enable more Erlang programs to work under McErlang, a methodology for writing properties that can be verified by McErlang, and a combination of simulation and model checking. The latter two features are illustrated by means of the messenger example found in the documentation of the Erlang/OTP distribution.

[HMCM09]
Ángel Herranz, Julio Mariño, Manuel Carro, and Juan José Moreno-Navarro. Modeling concurrent systems with shared resources. In Formal Methods for Industrial Critical Systems, 14th International Workshop, FMICS 2009, Eindhoven, The Netherlands, November 2-3, 2009. Proceedings, volume 5825 of Lecture Notes in Computer Science, pages 102--116, 2009. [ bib | http | .pdf ]
Testing is the more widely used approach to (partial) system validation in industry. The introduction of concurrency makes exhaustive testing extremely costly or just impossible, requiring shifting to formal verification techniques. We propose a methodology to design and verify a concurrent system that splits the verification problem in two independent tasks: internal verification of shared resources, where some concurrency aspects like mutual exclusion and conditional synchronisation are isolated, and external verification of processes, where synchronisation mechanisms are not relevant. Our method is language independent, non-intrusive for the development process, and improves the portability of the resulting system. We demonstrate it by actually checking several properties of an example application using the TLC model checker.

[BFIL09]
Clara Benac Earle, Lars-Åke Fredlund, J. Iglesias, and A. Ledezma. Verifying robocup teams. Electronic Notes in Theoretical Computer Science, 5348/2009:34--48, 2009. [ bib ]
[MHPCS09]
Susana Muñoz-Hernández, Víctor Pablos-Ceruelo, and Hannes Strass. Rfuzzy: An expressive simple fuzzy compiler. In Joan Cabestany, Francisco Sandoval, Alberto Prieto, and Juan M. Corchado, editors, IWANN (1), volume 5517 of Lecture Notes in Computer Science, pages 270--277. Springer, 2009. [ bib | DOI ]
[ALM09]
Gianluca Amato, James Lipton, and Robert McGrail. On the algebraic structure of declarative programming languages. Theoretical Computer Science, 410(46):4626--4671, 2009. [ bib | http ]
[MMNMH09]
Julio Mariño, Juan José Moreno-Navarro, and Susana Muñoz-Hernández. Implementing constructive intensional negation. New Generation Computing, 27(1):25--56, January 2009. [ bib ]
[GG09b]
Amaya García-Pérez and Álvaro García-Pérez. La afinación de la flauta tradicional de tres agujeros. Revista de Musicología, 22(2):343--361, 2009. [ bib ]

This file was generated by bibtex2html 1.98.