Search

Your search keyword '"MARTIN-MARTIN, ENRIQUE"' showing total 88 results
Start Over Author "MARTIN-MARTIN, ENRIQUE"
88 results on '"MARTIN-MARTIN, ENRIQUE"'

1. Formally Verified EVM Block-Optimizations

Author

Albert, Elvira, Genaim, Samir, Kirchner, Daniel, Martin-Martin, Enrique, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Enea, Constantin, editor, and Lal, Akash, editor

Published
2023
Full Text
View/download PDF

2. A Transformational Approach to Resource Analysis with Typed-norms Inference

Author

Albert, Elvira, Genaim, Samir, Gutiérrez, Raúl, and Martin-Martin, Enrique

Subjects
Computer Science - Programming Languages, Computer Science - Logic in Computer Science
Abstract

In order to automatically infer the resource consumption of programs, analyzers track how data sizes change along program's execution. Typically, analyzers measure the sizes of data by applying norms which are mappings from data to natural numbers that represent the sizes of the corresponding data. When norms are defined by taking type information into account, they are named typed-norms. This article presents a transformational approach to resource analysis with typed-norms that are inferred by a data-flow analysis. The analysis is based on a transformation of the program into an intermediate abstract program in which each variable is abstracted with respect to all considered norms which are valid for its type. We also present the data-flow analysis to automatically infer the required, useful, typed-norms from programs. Our analysis is formalized on a simple rule-based representation to which programs written in different programming paradigms (e.g., functional, logic, imperative) can be automatically translated. Experimental results on standard benchmarks used by other type-based analyzers show that our approach is both efficient and accurate in practice. Under consideration in Theory and Practice of Logic Programming (TPLP)., Comment: Under consideration in Theory and Practice of Logic Programming (TPLP)

Published
2019

3. Resource Analysis driven by (Conditional) Termination Proofs

Author

Albert, Elvira, Bofill, Miquel, Borralleras, Cristina, Martin-Martin, Enrique, and Rubio, Albert

Subjects
Computer Science - Programming Languages, Computer Science - Logic in Computer Science
Abstract

When programs feature a complex control flow, existing techniques for resource analysis produce cost relation systems (CRS) whose cost functions retain the complex flow of the program and, consequently, might not be solvable into closed-form upper bounds. This paper presents a novel approach to resource analysis that is driven by the result of a termination analysis. The fundamental idea is that the termination proof encapsulates the flows of the program which are relevant for the cost computation so that, by driving the generation of the CRS using the termination proof, we produce a linearly-bounded CRS (LB-CRS). A LB-CRS is composed of cost functions that are guaranteed to be locally bounded by linear ranking functions and thus greatly simplify the process of CRS solving. We have built a new resource analysis tool, named MaxCore, that is guided by the VeryMax termination analyzer and uses CoFloCo and PUBS as CRS solvers. Our experimental results on the set of benchmarks from the Complexity and Termination Competition 2019 for C Integer programs show that MaxCore outperforms all other resource analysis tools. Under consideration for acceptance in TPLP., Comment: Paper presented at the 35th International Conference on Logic Programming (ICLP 2019), Las Cruces, New Mexico, USA, 20-25 September 2019, 16 pages

Published
2019
Full Text
View/download PDF

5. Lower-Bound Synthesis Using Loop Specialization and Max-SMT

Author

Albert, Elvira, Genaim, Samir, Martin-Martin, Enrique, Merayo, Alicia, Rubio, Albert, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Woeginger, Gerhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Silva, Alexandra, editor, and Leino, K. Rustan M., editor

Published
2021
Full Text
View/download PDF

6. A Formal, Resource Consumption-Preserving Translation of Actors to Haskell

Author

Albert, Elvira, Bezirgiannis, Nikolaos, de Boer, Frank, and Martin-Martin, Enrique

Subjects
Computer Science - Programming Languages, Computer Science - Logic in Computer Science
Abstract

We present a formal translation of an actor-based language with cooperative scheduling to the functional language Haskell. The translation is proven correct with respect to a formal semantics of the source language and a high-level operational semantics of the target, i.e. a subset of Haskell. The main correctness theorem is expressed in terms of a simulation relation between the operational semantics of actor programs and their translation. This allows us to then prove that the resource consumption is preserved over this translation, as we establish an equivalence of the cost of the original and Haskell-translated execution traces., Comment: Pre-proceedings paper presented at the 26th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2016), Edinburgh, Scotland UK, 6-8 September 2016 (arXiv:1608.02534)

Published
2016

9. Rewriting and narrowing for constructor systems with call-time choice semantics

Author

López-Fraguas, Francisco J., Martin-Martin, Enrique, Rodríguez-Hortalá, Juan, and Sánchez-Hernández, Jaime

Subjects
Computer Science - Programming Languages
Abstract

Non-confluent and non-terminating constructor-based term rewrite systems are useful for the purpose of specification and programming. In particular, existing functional logic languages use such kind of rewrite systems to define possibly non-strict non-deterministic functions. The semantics adopted for non-determinism is call-time choice, whose combination with non-strictness is a non trivial issue, addressed years ago from a semantic point of view with the Constructor-based Rewriting Logic (CRWL), a well-known semantic framework commonly accepted as suitable semantic basis of modern functional logic languages. A drawback of CRWL is that it does not come with a proper notion of one-step reduction, which would be very useful to understand and reason about how computations proceed. In this paper we develop thoroughly the theory for the first order version of let-rewriting, a simple reduction notion close to that of classical term rewriting, but extended with a let-binding construction to adequately express the combination of call-time choice with non-strict semantics. Let-rewriting can be seen as a particular textual presentation of term graph rewriting. We investigate the properties of let-rewriting, most remarkably their equivalence with respect to a conservative extension of the CRWL-semantics coping with let-bindings, and we show by some case studies that having two interchangeable formal views (reduction/semantics) of the same language is a powerful reasoning tool. After that, we provide a notion of let-narrowing which is adequate for call-time choice as proved by soundness and completeness results of let-narrowing with respect to let-rewriting. Moreover, we relate those let-rewriting and let-narrowing relations (and hence CRWL) with ordinary term rewriting and narrowing (..) To appear in Theory and Practice of Logic Programming (TPLP)., Comment: 89 pages, 6 figures. To appear in Theory and Practice of Logic Programming (TPLP). Corrected typos

Published
2012

10. A Formal, Resource Consumption-Preserving Translation of Actors to Haskell

Author

Albert, Elvira, Bezirgiannis, Nikolaos, de Boer, Frank, Martin-Martin, Enrique, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Hermenegildo, Manuel V, editor, and Lopez-Garcia, Pedro, editor

Published
2017
Full Text
View/download PDF

11. Debugging Meets Testing in Erlang

Author

Tamarit, Salvador, Riesco, Adrián, Martin-Martin, Enrique, Caballero, Rafael, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Aichernig, Bernhard K., editor, and Furia, Carlo A., editor

Published
2016
Full Text
View/download PDF

12. Resource Analysis: From Sequential to Concurrent and Distributed Programs

Author

Albert, Elvira, Arenas, Puri, Correas, Jesús, Genaim, Samir, Gómez-Zamalloa, Miguel, Martin-Martin, Enrique, Puebla, Germán, Román-Díez, Guillermo, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Bjørner, Nikolaj, editor, and de Boer, Frank, editor

Published
2015
Full Text
View/download PDF

13. Static Inference of Transmission Data Sizes in Distributed Systems

Author

Albert, Elvira, Correas, Jesús, Martin-Martin, Enrique, Román-Díez, Guillermo, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Kobsa, Alfred, Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, and Margaria, Tiziana, editor

Published
2014
Full Text
View/download PDF

14. EDD: A Declarative Debugger for Sequential Erlang Programs

Author

Caballero, Rafael, Martin-Martin, Enrique, Riesco, Adrian, Tamarit, Salvador, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Ábrahám, Erika, editor, and Havelund, Klaus, editor

Published
2014
Full Text
View/download PDF

15. SACO: Static Analyzer for Concurrent Objects

Author

Albert, Elvira, Arenas, Puri, Flores-Montoya, Antonio, Genaim, Samir, Gómez-Zamalloa, Miguel, Martin-Martin, Enrique, Puebla, German, Román-Díez, Guillermo, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Ábrahám, Erika, editor, and Havelund, Klaus, editor

Published
2014
Full Text
View/download PDF

17. May-Happen-in-Parallel Analysis for Priority-Based Scheduling

Author

Albert, Elvira, Genaim, Samir, Martin-Martin, Enrique, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, McMillan, Ken, editor, Middeldorp, Aart, editor, and Voronkov, Andrei, editor

Published
2013
Full Text
View/download PDF

18. A Declarative Debugger for Sequential Erlang Programs

Author

Caballero, Rafael, Martin-Martin, Enrique, Riesco, Adrián, Tamarit, Salvador, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Veanes, Margus, editor, and Viganò, Luca, editor

Published
2013
Full Text
View/download PDF

20. Liberal Typing for Functional Logic Programs

Author

López-Fraguas, Francisco, Martin-Martin, Enrique, Rodríguez-Hortalá, Juan, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, and Ueda, Kazunori, editor

Published
2010
Full Text
View/download PDF

21. New Results on Type Systems for Functional Logic Programming

Author

López-Fraguas, Francisco J., Martin-Martin, Enrique, Rodríguez-Hortalá, Juan, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, and Escobar, Santiago, editor

Published
2010
Full Text
View/download PDF

29. SACO: Static Analyzer for Concurrent Objects

Author

Albert, Elvira, primary, Arenas, Puri, additional, Flores-Montoya, Antonio, additional, Genaim, Samir, additional, Gómez-Zamalloa, Miguel, additional, Martin-Martin, Enrique, additional, Puebla, German, additional, and Román-Díez, Guillermo, additional

Published
2014
Full Text
View/download PDF

41. A Formal, Resource Consumption-Preserving Translation from Actors with Cooperative Scheduling to Haskell*.

Author

Albert, Elvira, Bezirgiannis, Nikolaos, de Boer, Frank, Martin-Martin, Enrique, Hermenegildo, Manuel, López-García, Pedro, Pettorossi, Alberto, and Proietti, Maurizio

Subjects
SEMANTICS, TRANSLATIONS, LANGUAGE & languages, COOPERATIVE societies, PRAGMATICS
Abstract

We present a formal translation of a resource-aware extension of the Abstract Behavioral Specification (ABS) language to the functional language Haskell. ABS is an actor-based language tailored to the modeling of distributed systems. It combines asynchronous method calls with a suspend and resume mode of execution of the method invocations. To cater for the resulting cooperative scheduling of the method invocations of an actor, the translation exploits for the compilation of ABS methods Haskell functions with continuations. The main result of this article is a correctness proof of the translation by means of a simulation relation between a formal semantics of the source language and a high-level operational semantics of the target language, i.e., a subset of Haskell. We further prove that the resource consumption of an ABS program extended with a cost model is preserved over this translation, as we establish an equivalence of the cost of executing the ABS program and its corresponding Haskell-translation. Concretely, the resources consumed by the original ABS program and those consumed by the Haskell program are the same, considering a cost model. Consequently, the resource bounds automatically inferred for ABS programs extended with a cost model, using resource analysis tools, are sound resource bounds also for the translated Haskell programs. Our experimental evaluation confirms the resource preservation over a set of benchmarks featuring different asymptotic costs. [ABSTRACT FROM AUTHOR]

Published
2020
Full Text
View/download PDF

42. A Transformational Approach to Resource Analysis with Typed-norms Inference.

Author

ALBERT, ELVIRA, GENAIM, SAMIR, GUTIÉRREZ, RAÚL, and MARTIN-MARTIN, ENRIQUE

Subjects
NATURAL numbers, PROGRAM transformation, DATA mapping
Abstract

In order to automatically infer the resource consumption of programs, analyzers track how data sizes change along program's execution. Typically, analyzers measure the sizes of data by applying norms which are mappings from data to natural numbers that represent the sizes of the corresponding data. When norms are defined by taking type information into account, they are named typed-norms. This article presents a transformational approach to resource analysis with typed-norms that are inferred by a data-flow analysis. The analysis is based on a transformation of the program into an intermediate abstract program in which each variable is abstracted with respect to all considered norms which are valid for its type. We also present the data-flow analysis to automatically infer the required, useful, typed-norms from programs. Our analysis is formalized on a simple rule-based representation to which programs written in different programming paradigms (e.g., functional, logic, and imperative) can be automatically translated. Experimental results on standard benchmarks used by other type-based analyzers show that our approach is both efficient and accurate in practice. [ABSTRACT FROM AUTHOR]

Published
2020
Full Text
View/download PDF

45. A Formal, Resource Consumption-Preserving Translation of Actors to Haskell

Author

Bezirgiannis, N. (Nikolaos), Boer, F.S. (Frank) de, E. Albert (Erlvira), E. Martin-Martin (Enrique), Bezirgiannis, N. (Nikolaos), Boer, F.S. (Frank) de, E. Albert (Erlvira), and E. Martin-Martin (Enrique)

Abstract

We present a formal translation of an actor-based language with cooperative scheduling to the functional language Haskell. The translation is proven correct with respect to a formal semantics of the source language and a high-level operational semantics of the target, i.e. a subset of Haskell. The main correctness theorem is expressed in terms of a simulation relation between the operational semantics of actor programs and their translation. This allows us to then prove that the resource consumption is preserved over this translation, as we establish an equivalence of the cost of the original and Haskell-translated execution traces.

Published
2016

46. FLOP: A User-Friendly System for Automated Program Assessment

Author

Llana, Luis, Martin-Martin, Enrique, and Velázquez-Iturbide, J.

Subjects
FLOP, learning of programming, automated assessment systems, user-centered design
Abstract

Currently, automated systems for program submission and assessment play a central role in the teaching of programming. A number of such systems have been developed in the last two decades. However, their adoption in regular programming teaching presents an obstacle: the overhead work required for the design of each problem, for compilation of problem collections, and for mundane management tasks. An open challenge is to make these systems easier to use and to reduce to a minimum the number of management tasks. In this article we present the FLOP system, which was developed to satisfy this goal. The contribution of the article is twofold. On the one hand, we present the FLOP system itself and its user-friendly features. On the other hand, we present in detail the user-centered design process used to design and enhance the ease of use of FLOP. Several actions were undertaken to inquire users' concerns and needs, with a usability evaluation of FLOP conducted with students being the most fruitful action.

Published
2014

48. Type Classes in Functional Logic Programming (Author’s version for E-Prints Complutense)

Author

Martin-Martin, Enrique

Subjects
Lenguajes de programación
Abstract

Type classes provide a clean, modular and elegant way of writing overloaded functions. Functional logic programming languages (FLP in short) like Toy or Curry have adopted the Damas-Milner type system, so it seems natural to adopt also type classes in FLP. However, type classes has been barely introduced in FLP. A reason for this lack of success is that the usual translation of type classes using dictionaries presents some problems in FLP like the absence of expected answers due to a bad interaction of dictionaries with the call-time choice semantics for non-determinism adopted in FLP systems. In this paper we present a type-passing translation of type classes based on type-indexed functions and type witnesses that is well-typed with respect to a new liberal type system recently proposed for FLP. We argue the suitability of this translation for FLP because it improves the dictionary-based one in three aspects. First, it obtains programs which run as fast or faster—with an speedup from 1.05 to 2.30 in our experiments. Second, it solves the mentioned problem of missing answers. Finally, the proposed translation generates shorter and simpler programs. (C) ACM, (2011). This is the authors version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in PEPM ’11 Proceedings of the 20th ACM SIGPLAN workshop on Partial evaluation and program manipulation (January 24–25, 2011, Austin, Texas, USA). http://doi.acm.org/10.1145/1929501.1929524.

Published
2011

Catalog

Books, media, physical & digital resources
See catalog results