@article{2017:GPNS:JFP,
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
calculus},
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 = {}
}

@article{glm2017:fac,
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-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}
}

@inproceedings{Tamarit2016:EPTCS,
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}
}

@inproceedings{Vigueras2016:EPTCS,
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}
}

@inbook{ViguerasML:2017:HLRS,
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}
}

@article{Gallina2016,
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},
internacional = {yes},
isi-jcr = {yes}
}

@article{Marino2017:srcodegeneration,
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 templates.},
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.