ResumenA type derivation system for ErlangLópez-Fraguas, Francisco Javier; Montenegro, Manuel; Suárez-García, Gorka. Actas de las XVII Jornadas de Programación y Lenguajes (PROLE 2017), 2017-07-19.Erlang is a dynamically typed concurrent functional language of increasing interest in industry and academy. Official Erlang distributions come equipped with Dialyzer a useful static analysis tool able to anticipate runtime errors by inferring so-called success types, which are overapproximations to the real semantics of expressions. However, Dialyzer exhibits two main weaknesses: on the practical side, its ability to deal with functions that are typically polymorphic is rather poor; and on the theoretical side, a fully developed theory for its underlying type system –comparable to, say, Hindley-Milner system– does not seem to exist, something that we consider a regrettable circumstance. This work in progress is the starting point of a medium-term project aiming at improving both aspects, so that at its end we should have proposed a full type system able to infer polymorphic success types for Erlang programs, accompanied by solid theoretical foundations including adequateness results for the type system. In this first step we only provide a derivation system of monomorphic success types for Erlang, along with correctness results with respect to a suitable semantics for the language. ArtículoTowards the Automatic Verification of QCSP tractability resultsAbuin, Alex; Chen, Hubie; Hermo, Montserrat; Lucio, Paqui. Actas de las XVII Jornadas de Programación y Lenguajes (PROLE 2017), 2017-07-19.We deal with the quantied constraint satisfaction problem (QCSP) which consists in deciding, given an structure and a rst-order sentence built from atoms, with conjunction and quantication, whether or not the sentence is true on the structure. We study a known proof system which has been used to derive QCSP tractability results. Our contribution is to formalize this proof system into an automatically veried theory, so that it can be used (in a near future) as a basis for automatically verify tractability results. ResumenDescription and Evaluation of a Generic Design to Integrate CLP and Tabled ExecutionArias, Joaquín; Carro, Manuel. Actas de las XVII Jornadas de Programación y Lenguajes (PROLE 2017), 2017-07-19.Logic programming systems with tabling and constraints (TCLP, tabled constraint logic programming) have been shown to be more expressive and in some cases more efficient than those featuring only either tabling or constraints. Previous implementations of TCLP systems which use entailment to determine call / answer subsumption did not provide a simple, uniform, and well-documented interface to facilitate the integration of additional constraint solvers in existing tabling systems, which would increase the application range of TCLP. We present the design and an experimental evaluation of Mod TCLP, a framework which eases this integration. Mod TCLP views the constraints solver as a client of the tabling system. The tabling system is generic w.r.t. the constraint solver and only requires a clear, small interface from the latter. We validate our design by integrating four constraint solvers: a re-engineered version of a previously existing constraint solver for difference constraints, written in C; the standard versions of Holzbauer’s CLP(Q) and CLP(R), written in Prolog; and a new constraint solver for equations over finite lattices. We evaluate the performance of our framework in several benchmarks using the aforementioned constraint solvers. All the development work and evaluation was done in Ciao Prolog.