@inproceedings{TechPeopleCareICERI2019,
  author = {Mu{\~n}oz Hern{\'a}ndez, S. and Benac Earle, C. and Carrillo Plaza, J.E.},
  title = {TECHPEOPLECARE: INNOVATIVE DIGITAL LITERACY TRAINING METHODOLOGY},
  series = {12th International Conference of Education, Research and Innovation},
  booktitle = {ICERI2019 Proceedings},
  isbn = {978-84-09-14755-7},
  issn = {2340-1095},
  publisher = {IATED},
  location = {Seville, SPAIN},
  month = {11th-13th November},
  year = {2019},
  pages = {3496-3499}
}

@inproceedings{BENFRED2019,
  author = {Clara Benac Earle and Lars{-}{\AA}ke Fredlund},
  title = {A Property-based Testing Framework for Multi-Agent Systems},
  booktitle = {Proceedings of the 18th International Conference on
                  Autonomous Agents and MultiAgent Systems, {AAMAS}
                  2019},
  pages = {},
  year = {2019},
  url = {},
  doi = {},
  timestamp = {},
  biburl = {},
  note = {accepted as Extended Abstract},
  bibsource = {}
}

@comment{{Al final apareció en 2018}}

@article{2019:GPNS:JFP,
  tipoactividad = {Artículos en revistas},
  internacional = {yes},
  author = {{{\'{A}}lvaro} {Garc{\'{i}}a-P{\'{e}}rez} and Pablo Nogueira},
  title = {The full-reducing {K}rivine abstract machine {KN} simulates
                  pure normal-order in lockstep: {A} proof via corresponding
                  calculus},
  journal = {Journal of Functional Programming},
  year = {2019},
  abstract = {We exploit the idea of proving properties of an abstract
                  machine by using a corresponding semantic artefact better
                  suited to their proof. The abstract machine is an improved
                  version of Pierre Crégut's full-reducing Krivine machine
                  KN. The original version works with closed terms of the pure
                  lambda calculus with de Bruijn indices. The improved version
                  reduces in similar fashion but works on closures where terms
                  may be open. The corresponding semantic artefact is a
                  structural operational semantics of a calculus of closures
                  whose reduction relation is purposely a reduction
                  strategy. As shown in previous work, improved KN and the
                  structural operational semantics `correspond', i.e. both
                  artefacts realise the same reduction strategy.  In this
                  paper we prove in the calculus of closures that the
                  reduction strategy simulates in lockstep (at every reduction
                  step) the complete and standard 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 of the closure calculus to pure terms
                  of the pure lambda calculus. Thus, KN also simulates
                  normal-order in lockstep by the correspondence. This result
                  is stronger than the known proof that KN is complete, for in
                  the pure lambda calculus there are complete but non-standard
                  strategies. The lockstep simulation proof consists of
                  straightforward structural inductions thanks to three
                  properties of the closure calculus we call `index
                  alignment', `parameters-as-levels', and `balanced
                  derivations'. The first two come from KN. Thanks to these
                  properties a proof in a calculus of closures involving de
                  Bruijn indices and de Bruijn levels is unproblematic. There
                  is no lexical adjustment at binding lookup, on-the-fly
                  alpha-conversion, or recursive traversals of the term to
                  deal with bound and free variables as in other calculi. This
                  paper contributes to the framework for environment machines
                  of Biernacka and Danvy a full-reducing open-terms closure
                  calculus, its corresponding abstract machine, and a lockstep
                  simulation proof via a substitution function.},
  issn = {0956-7968 (Print),1469-7653 (Online)},
  url = {http://dx.doi.org/10.1017/S0956796819000017},
  volume = {29},
  pages = {e7}
}

@comment{{2015}}

This file was generated by bibtex2html 1.98.