author = {Jamal Abdelhameed, Huda and Mu{\~{n}}oz-Hern{\'{a}}ndez, Susana},
  booktitle = {2017 Joint International Conference on Information and Communication Technologies for Education and Training and International Conference on Computing in Arabic (ICCA-TICET)},
  title = {Emotion and opinion retrieval from social media in Arabic language: Survey},
  series = {IEEE Xplore},
  publisher = {IEEE},
  year = {2017},
  month = {August},
  address = {Khartoum, Sudan},
  pages = {1-8},
  url = {http://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=8095291&isnumber=8095284},
  doi = {10.1109/ICCA-TICET.2017.8095291},
  isbn = {978-1-5386-2226-1}
  author = {Mu{\~{n}}oz-Hern{\'{a}}ndez, Susana},
  booktitle = {12th International Conference on ICT for Development, Education and Training. E-learning Africa},
  title = {Lets remove digital illiteracy from African rural areas},
  address = {Republic of Mauritius},
  year = {2017},
  month = {September}
  author = {Elhadi Elsiddig Mahmoud, Sara and Mu{\~{n}}oz-Hern{\'{a}}ndez, Susana},
  booktitle = {Fuzzy Systems and Data Mining III},
  title = {Asthma Severity Diagnosis System Based on Fuzzy Reasoning},
  series = {Frontiers in Artificial Intelligence and Applications (FAIA)},
  editor = {Tallón-Ballesteros, A.J. Li K.},
  publisher = {IOS Press},
  volume = {299},
  year = {2017},
  month = {November},
  address = {Hualien, Taiwan},
  pages = {197-202},
  doi = {10.3233/978-1-61499-828-0-197},
  isbn = {978-1-61499-827-3}
  tipoactividad = {Artículos en revistas},
  internacional = {yes},
  author = {{{\'{A}}lvaro} {Garc{\'{i}}a-P{\'{e}}rez} and Pablo Nogueira
                  and Pierre-Yves Strub},
  title = {The full-reducing {K}rivine machine simulates normal order
                  in lockstep: a mechanised proof via the corresponding
  journal = {Journal of Functional Programming},
  year = {2017},
  abstract = {We exploit the idea of proving properties of an abstract
                  machine by using a corresponding semantic style that better
                  suits the purpose. In a previous work we introduced a
                  calculus of closures and proved by program derivation that
                  it corresponds to a slightly optimised open-terms version of
                  Pierre Crégut's full-reducing Krivine machine KN. In this
                  work we prove that this calculus (and KN by correspondence)
                  simulates in lockstep the standard and complete normal-order
                  strategy (i.e. leftmost reduction to normal form) of the
                  pure lambda calculus.  The simulation is witnessed by a
                  substitution function from closures to pure terms. Lockstep
                  simulation is stronger than the known proof that KN is
                  complete, for in the pure lambda calculus there are complete
                  but non-standard strategies. The proof of lockstep
                  simulation proceeds by straightforward structural induction
                  thanks to how KN's parameters-as-levels and index-alignment
                  properties are carried into the calculus' deterministic
                  reduction relation, allowing `balanced derivations' where
                  the nesting level under lambda at which reduction is taking
                  place remains constant at both sides of a reduction.
                  Lexical adjustments at binding lookup, on-the-fly
                  alpha-conversion, or recursive traversals (as in the locally
                  nameless representation) are unnecessary. The proof's
                  lemmata constitute a recipe for carrying
                  parameters-as-levels, index alignment, and balanced
                  derivations to other calculi and machines. The whole proof,
                  including the closure calculus and normal-order, has been
                  mechanised in the Coq proof assistant and is available
                  online. This work amends the framework for environment
                  machines of Biernacka and Danvy, adding a missing
                  full-reducing open-terms closure calculus, machine, and
                  lockstep simulation proof via a substitution function.},
  alturl = {},
  altpdf = {},
  altps = {},
  issn = {0956-7968 (print),1469-7653 (Online)},
  optkey = {},
  optvolume = {},
  optnumber = {},
  optpages = {},
  optmonth = {},
  note = {Submitted and in revision},
  optannote = {}
  abstract = {We present a declarative framework for the
                  compilation of constraint logic programs into
                  variable-free relational theories which are then
                  executed by rewriting. This translation provides an
                  algebraic formulation of the abstract syntax of
                  logic programs. Logic variables, unification, and
                  renaming apart are completely elided in favor of
                  manipulation of variable-free relation
                  expressions. In this setting, term rewriting not
                  only provides an operational semantics for logic
                  programs, but also a simple framework for reasoning
                  about program execution. We prove the translation
                  sound, and the rewriting system complete with
                  respect to traditional SLD semantics.},
  author = {Gallego Arias, Emilio Jes{\'u}s and Lipton, James and Mari{\~n}o, Julio},
  da = {2017//},
  date-added = {2017-03-31 13:45:17 +0000},
  date-modified = {2017-03-31 13:45:17 +0000},
  doi = {10.1007/s00165-016-0369-z},
  id = {Gallego Arias2017},
  isbn = {1433-299X},
  journal = {Formal Aspects of Computing},
  number = {1},
  pages = {97--124},
  title = {Constraint logic programming with a relational machine},
  ty = {JOUR},
  url = {http://dx.doi.org/10.1007/s00165-016-0369-z},
  volume = {29},
  year = {2017},
  bdsk-url-1 = {http://dx.doi.org/10.1007/s00165-016-0369-z}
  author = {Tamarit, Salvador and Mari\~no, Julio and Vigueras, Guillermo and Carro, Manuel},
  year = {2017},
  title = {Towards a Semantics-Aware Code Transformation Toolchain for Heterogeneous Systems},
  editor = {Villanueva, Alicia},
  booktitle = {{\rm Proceedings XVI Jornadas sobre}
               Programaci\'on y Lenguajes,
               {\rm Salamanca, Spain, 14-16th September 2016}},
  series = {Electronic Proceedings in Theoretical Computer Science},
  volume = {237},
  publisher = {Open Publishing Association},
  pages = {34-51},
  doi = {10.4204/EPTCS.237.3}
  author = {Vigueras, Guillermo and Carro, Manuel and Tamarit, Salvador and Mari\~no, Julio},
  year = {2017},
  title = {Towards Automatic Learning of Heuristics for Mechanical Transformations of Procedural Code},
  editor = {Villanueva, Alicia},
  booktitle = {{\rm Proceedings XVI Jornadas sobre}
               Programaci\'on y Lenguajes,
               {\rm Salamanca, Spain, 14-16th September 2016}},
  series = {Electronic Proceedings in Theoretical Computer Science},
  volume = {237},
  publisher = {Open Publishing Association},
  pages = {52-67},
  doi = {10.4204/EPTCS.237.4}
  editor = {C. Niethammer and J. Gracia and T. Hilbrich and
                  A. Knüpfer and M.M. Resch and W.E. Nagel},
  title = {Tools for High Performance Computing 2016},
  chapter = {Machine Learning-Driven Automatic Program
                  Transformation to Increase Performance in
                  Heterogeneous Architectures},
  publisher = {Springer},
  year = 2017,
  note = {In press},
  isbn = {978-3-319-56701-3}
  title = {Promoting {MBA} in the rail sector by deriving process-related evidence via {MDSafeCer}},
  journal = {Computer Standards \& Interfaces },
  volume = {54},
  pages = {119--128},
  year = {2017},
  issn = {0920-5489},
  doi = {http://dx.doi.org/10.1016/j.csi.2016.11.007},
  author = {Gallina, Barbara and G{\'{o}}mez{-}Mart{\'{\i}}nez, Elena and Benac Earle, Clara},
  tipoactividad = {Art{\'{i}}culos en revistas},
  internacional = {yes},
  isi-jcr = {yes}
  author = {Mari{\~{n}}o, Julio
         and Alborodo, Ra{\'u}l N. N.
         and Fredlund, Lars-{\AA}ke
         and Herranz, {\'A}ngel},
  title = {Synthesis of verifiable concurrent Java components from formal models},
  journal = {Software {\&} Systems Modeling},
  year = {2017},
  pages = {1--35},
  abstract = {Concurrent systems are hard to program, and ensuring
                  quality by means of traditional testing techniques
                  is often very hard as errors may not show up easily
                  and reproducing them is hard. In previous work, we
                  have advocated a model-driven approach to the
                  analysis and design of concurrent, safety-critical
                  systems. However, to take full advantage of these
                  techniques, they must be supported by code
                  generation schemes for concrete programming
                  languages. Ideally, this translation should be
                  traceable, automated and should support the
                  verification of the generated code. In our work, we
                  consider the problem of generating a concurrent Java
                  component from a high-level model of inter-process
                  interaction (i.e., communication +
                  synchronization). We call our formalism shared
                  resources. From the model, which can be represented
                  in mathematical notation or written as a Java
                  interface annotated using an extension of JML, a
                  Java component can be obtained by a semiautomatic
                  translation. We describe how to obtain shared memory
                  (using a priority monitors library) and message
                  passing (using the JCSP library)
                  implementations. Focusing on inter-process
                  interaction for formal development is justified by
                  several reasons, e.g., mathematical models are
                  language-independent and allow to analyze certain
                  concurrency issues, such as deadlocks or liveness
                  properties prior to code generation. Also, the Java
                  components produced from the shared resource model
                  will contain all the concurrency-related language
                  constructs, which are often responsible for many of
                  the errors in concurrent software. We follow a
                  realistic approach where the translation is
                  semiautomatic (schemata for code generation) and the
                  programmer still retains the power of coding or
                  modifying parts of the code for the resource. The
                  code thus obtained is JML-annotated Java with proof
                  obligations that help with code traceability and
                  verification of safety and liveness properties. As
                  the code thus obtained is not automatically correct,
                  there is still the need to verify its conformance to
                  the original specs. We illustrate the methodology by
                  developing a concurrent control system and verifying
                  the code obtained using the KeY program verification
                  tool. We also show how KeY can be used to find
                  errors resulting from a wrong use of the
  issn = {1619-1374},
  doi = {10.1007/s10270-017-0581-1},
  url = {http://dx.doi.org/10.1007/s10270-017-0581-1}

This file was generated by bibtex2html 1.98.