%================================================== % Bibtex %================================================== @InProceedings{moshier02, author = {M. A. Moshier and A. Jung}, title = {A Logic for Probabilities in Semantics}, booktitle = {Computer Science Logic}, editor = {Julian Bradfield}, publisher = sv, series = lncs, volume = 2471, pages = {216--231}, year = 2002 } @inproceedings{BS03a, author = {A. Bauer and A. Simpson}, title = {Locally Non-compact Spaces and Continuity Principles}, booktitle = {Computability and Complexity in Analysis}, year = 2003} @unpublished{BS03b, author = {A. Bauer and A. Simpson}, title = {Two Constructive Embedding-Extension Theorems with Applications to Continuity Principles and to Banach-Mazur Computability}, note = {Submitted}, year = {2003}} @unpublished{ELS03, author = {M. Escard\'o, J. Lawson and A. Simpson}, title = {Comparing Cartesian-closed Categories of (Core) Compactly Generated Spaces}, note = {Submitted}, year = {2003}} @inproceedings{Sim03, author = {A. Simpson}, title = {Towards a Convenient Category of Topological Domains}, booktitle = {Thirteenth {ALGI} Workshop}, publisher = {{RIMS}, Kyoto University}, year = {2003}} @Unpublished{escardo:bellairs, author = {M.H. Escard\'o}, title = {Topology of data types and computability concepts}, note = {94 pages, School of Computer Science, University of Birmingham, submitted to the proceedings of the \emph{Workshop on Domain Theoretic Methods in Probabilistic Processes}, McGill University's Bellairs research institute, Barbados, April 21-25 2003. \url{http://www.cs.bham.ac.uk/~mhe/papers/barbados.pdf}}, month = {Oct}, year = 2003 } @InProceedings{EP03, author = {Edalat, A. and Pattinson, D.}, title = {Initial value problems in domain theory}, booktitle = {Proceedings of Computability and Complexity in Analysis}, year = 2003 } @InProceedings{KA03, author = {Khanban, A. A. and Edalat, A.}, title = {Computing {D}elaunay triangulation with imprecise data}, booktitle = {Proceedings of the 15th Canadian Computational Geometry}, year = 2003, address = {Halifax} } @Unpublished{jung03, author = {A. Jung}, title = {Stably compact spaces and the probabilistic powerspace construction}, note = {Under review for ENTCS vol.\ 87}, year = 2003 } @Article{keimel05, author = {K. Keimel and J. D. Lawson}, title = {Measure extension theorems for $T_0$-spaces}, journal = ta, year = 2005, volume = 149, pages = {57--83} } @Unpublished{farjudian03a, author = {Amin Farjudian}, title = {Sequentiality of wRPCF}, note = {Presented in the Workshop Domains VI, Birmingham, September 16--19, 2002} } @Unpublished{farjudian03b, author = {Amin Farjudian}, title = {Conservativity of wRPCF over PCF}, note = {Presented in BCTCS 19, Leicester, England, April 7--9, 2003} } @Unpublished{tix+:semantic-domains-prob-nondet, author = {Regina Tix and Klaus Keimel and Gordon Plotkin}, title = {Semantic Domains for Combining Probability and Non-Determinism}, note = {Draft available online}, ps = {http://homepages.inf.ed.ac.uk/gdp/publications/tkp.ps}, url = {http://homepages.inf.ed.ac.uk/gdp/publications/}, theme = {I}, site = {edinburgh,darmstadt} } @Article{escardo04, author = {M. H. Escardó and M. Hofmann and {Th.} Streicher}, title = {On the non-sequential nature of the interval-domain model of real-number computation}, journal = mscs, year = 2004, volume = 14, pages = {803--814} } @article{alvarez04, author = {M. Alvarez-Manilla and A. Jung and K. Keimel}, title = {The probabilistic powerdomain for stably compact spaces}, journal = tcs, year = 2004, volume = 328, publisher = elsevier, pages = {221--244} } @InProceedings{jung04, author = {A. Jung}, title = {Stably compact spaces and the probabilistic powerspace construction}, booktitle = {Domain-theoretic Methods in Probabilistic Processes}, year = 2004, editor = {J. Desharnais and P. Panangaden}, volume = 87, series = entcs, publisher = elsevier, note = {15pp.} } @inProceedings{keimel04, author = {K. Keimel}, title = {The probabilistic powerdomain for the upwards topology of compact ordered spaces}, year = 2004, editor = {J. Desharnais and P. Panangaden}, volume = 87, pages = {225--238}, series = entcs, publisher = elsevier } @InProceedings{escardo04b, author = {M. H. Escard\'o}, title = {Synthetic topology of data types and classical spaces}, booktitle = {Domain-theoretic Methods in Probabilistic Processes}, year = 2004, editor = {J. Desharnais and P. Panangaden}, pages = {21--156}, volume = 87, series = entcs, publisher = elsevier } @PhdThesis{farjudian04, author = {A. Farjudian}, title = {Sequentiality in real number computation}, school = {University of Birmingham}, year = 2004 } @PhdThesis{marcial04, author = {J. R. Marcial-Romero}, title = {Semantics of a sequential language for exact real-number computation}, school = {University of Birmingham}, year = 2004 } @InProceedings{zawawy06, author = {M. A. El-Zawawy and A. Jung}, title = {Priestley duality for strong proximity lattices}, booktitle = {Proceedings of the 22nd Annual Conference on Mathematical Foundations of Programming Semantics (MFPS XXII)}, pages = {199--217}, year = 2006, editor = {S. Brookes and M. Mislove}, volume = 158, series = entcs, publisher = elsevier } % From Birmingham @string{lncs = "Lecture Notes in Computer Science"} @InProceedings(Reddy-Yang-heap, Author = "Reddy, U. S. and Yang, H.", Title = "Correctness of Data Representations involving Heap Data Structures", BookTitle = "Programming Languages and Systems: 12th European Symposium on Programming", Publisher = "Springer-Verlag", Series = lncs, Volume = "2618", Pages = "223-237", Year = "2003" ) @Article(Reddy-Yang-SCP, Author = "Reddy, U. S. and Yang, H.", Title = "Correctness of Data Representations involving Heap Data Structures", Journal = "Science of Computer Programming", Volume = "", Number = "", Month = "", Pages = "(to appear)", Year = "2004" ) % From Cambridge @Unpublished{bierman03:_unify, author = {G.M. Bierman and E. Meijer and W. Schulte}, title = {Unifying tables, objects and documents}, note = {To appear in proceedings of DP-COOL 2003}, year = 2003 } @Unpublished{bierman03:_xen, author = {G.M. Bierman and E. Meijer and W. Schulte}, title = {The essence of Xen}, note = {Paper submitted for publication}, year = 2003 } @InProceedings{bierman03:_progr, author = {G.M. Bierman and E. Meijer and W. Schulte}, title = {Programming with circles, triangles and rectangles}, booktitle = {Proceedings of XML 2003}, year = 2003 } @InProceedings{bierman03:_dynam, author = {G. Bierman and M. Hicks and P. Sewell and G. Stoyle and K. Wansborough}, title = {Dynamic rebinding for marshalling and update, with destruct-time lambda}, booktitle = {Proceedings of ACM ICFP}, pages = {99--110}, year = 2003 } @TechReport{bierman03:_mj, author = {G.M. Bierman and M. Parkinson and A. Pitts}, title = {MJ: An imperative core calculus for Java and Java with effects}, institution = {University of Cambridge Computer Laboratory}, year = 2003, number = 563 } @InProceedings{bierman03:_effec_java, author = {G.M. Bierman and M. Parkinson}, title = {Effects and effect inference for a core Java calculus}, booktitle = {Proceedings of Workshop on Object-Oriented Developments}, year = 2003, volume = 82, number = 8, series = {ENTCS} } @InProceedings{bierman03:_formal_exten_abstr, author = {G.M. Bierman and M. Hicks and P. Sewell and G. Stoyle}, title = {Formalizing dynamic software updating (Extended Abstract)}, booktitle = {Proceedings of Workshop on Unexpected Software Evolution}, year = 2003 } % Chalmers (Nothing) % Darmstadt % DIKU (Nothing) % Sussex @INPROCEEDINGS{Reus:MSaLC, author = {B.~Reus}, title = {Modular Semantics and Logics of Classes}, booktitle = "Computer Science Logic", pages = "456--469", editors = "Matthias Baatz and Johann A. Makowsky", publisher = "Springer Verlag", Series = LNCS, volume = "2803", Address = "Berlin", year = "2003"} % TCS(316):191-213, 2004 @article{ReusStr:TCS, author = {B.~Reus and Th.~Streicher}, title = "Semantics and Logics of Object Calculi", journal = {TCS}, volume = "316", number = "1--3", pages = "191--213", year = 2004 , month = may, OPTnote = "to appear" } @INPROCEEDINGS{Reus:CBvOB, author = {B.~Reus}, title = {Class based vs.~Object based: A Denotational Comparison}, booktitle = "Algebraic Methodology And Software Technology", pages = "473-488", editors = "H.~Kirchner and Ch.~Ringeissen", publisher = "Springer Verlag", Series = LNCS, volume = "2422", Address = "Berlin", year = "2002"} % Edinburgh @InProceedings{wolverson:ocamelot03, author = {Nicholas Wolverson}, title = {{O'Camelot}: Adding Objects to a Resource Aware Functional Language}, booktitle = {TFP 2003: On-site Proceedings of the Fourth Symposium on Trends in Functional Programming}, year = 2003, month = sep, url = {http://homepages.inf.ed.ac.uk/stg/workshops/TFP/} } % Genoa @InProceedings{ancona03:_mixin, author = {D.~Ancona and S.~Fagorzi and E.~Moggi and E.~Zucca}, title = {Mixin modules and computational effects}, booktitle = {Proceedings of ICALP}, year = 2003, volume = 2719, series = {LNCS} } @InProceedings{ancona03:_stron_typin_separ_compil_java_languag, author = {D.~Ancona and G.~Lagorio.}, title = {Stronger Typings for Separate Compilation of Java-like Languages}, booktitle = {Workshop on Formal Techniques for Java-like Programs}, year = 2003 } @InProceedings{drossopoulou03:_flexib_model_dynam_linkin, author = {S.~Drossopoulou and G.~Lagorio and S.~Eisenbach}, title = {Flexible Models for Dynamic Linking}, booktitle = {Proceedings of ESOP}, year = 2003, volume = 2618, series = {LNCS} } @InProceedings{ancona03:_calcul_dynam_linkin, author = {D.~Ancona D., S.~Fagorzi, E.~Zucca}, title = {A Calculus for Dynamic Linking}, booktitle = {Proceedings of ICTCS}, year = 2003, volume = 2841, series = {LNCS} } @InProceedings{lagorio03:_towar_smart_compil_manag_java, author = {G.~Lagorio}, title = {Towards a Smart Compilation Manager for Java}, booktitle = {Proceedings of ICTCS}, year = 2003, volume = 2841, series = {LNCS} } @Unpublished{ancona:_princ_typin_java_languag, author = {D.~Ancona, E.~Zucca}, title = {Principal Typings for Java-like Languages}, note = {To appear in POPL 2004} } % Inria @INPROCEEDINGS{Hirschowitz-Leroy-Wells-PPDP, AUTHOR = {Tom Hirschowitz and Xavier Leroy and Joe B. Wells}, TITLE = {Compilation of extended recursion in call-by-value functional languages}, BOOKTITLE = {International Conference on Principles and Practice of Declarative Programming}, YEAR = 2003, PAGES = {160--171}, PUBLISHER = {ACM Press}, URL = {http://pauillac.inria.fr/~xleroy/publi/compil-recursion.pdf} } @TECHREPORT{Hirschowitz-Leroy-Wells-mm-tr, AUTHOR = {Tom Hirschowitz and Xavier Leroy and Joe B. Wells}, TITLE = {A reduction semantics for call-by-value mixin modules }, INSTITUTION = {INRIA}, YEAR = 2003, NUMBER = 4682, URL = {ftp://ftp.inria.fr/INRIA/publication/publi-pdf/RR/RR-4682.pdf} } @TECHREPORT{Hirschowitz-Leroy-Wells-rec-tr, AUTHOR = {Tom Hirschowitz and Xavier Leroy and Joe B. Wells}, TITLE = {On the implementation of recursion in call-by-value functional languages}, INSTITUTION = {INRIA}, YEAR = 2003, NUMBER = 4728, URL = {ftp://ftp.inria.fr/INRIA/publication/publi-pdf/RR/RR-4728.pdf} } @ARTICLE{Bonniot-ENTCS, AUTHOR = {Daniel Bonniot}, TITLE = {Using kinds to type partially-polymorphic methods}, JOURNAL = {Electronic Notes in Theoretical Computer Science}, VOLUME = {75}, PUBLISHER = {Elsevier}, EDITOR = {Gilles Barthe and Peter Thiemann}, YEAR = {2003} } % LMU Munich @Unpublished{david03:_resour_progr_logic_grail, author = {David Aspinall and Lennart Beringer and Martin Hofmann, Hans-Wolfgang Loidl and Alberto Momigliano}, title = {A Resource-aware Program-Logic for Grail}, year = 2003, note = {Draft paper} } % Loria (Nothing) @InProceedings{clm:lpar03, author = "A. Ciaffaglione. and L. Liquori and M. Miculan", title = "Imperative Object-based Calculi in (Co)Inductive Type Theories", booktitle = "Proc. of LPAR'03", Series = LNCS, Volume = "2850", year = "2003", editor = "M. Vardi and A. Voronkov", address = "Almaty, Kazakhst=an" } @InProceedings{clm:merlin03, author = "A. Ciaffaglione and L. Liquori and M. Miculan", title = "Reasoning on an Imperative Object-based Calculus in Higher Order Abstract Syntax'", booktitle = "Proc.~2nd~MER$\lambda$IN", year = 2003 } @PhdThesis{ciaffa:phd, author = "A. Ciaffaglione", title = "Reasoning on real numbers and objects in {L}ogical {F}rameworks", school = "Dipartimento di Matematica e Informatica, Universit\`a di Udine", year = "Italy" } % Minho (Nothing) % Nottingham % Oxford @inproceedings{Gibbons2003:Patterns, author="Jeremy Gibbons", title="Patterns in Datatype-Generic Programming", booktitle="Declative Programming in the Context of Object-Oriented Languages", editor="Jörg Striegnitz", year="2003", month="August", url="http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/index .html#patterns" } % Pisa (Nothing?) % Tallinn (Nothing) % Paris (nothing) % QMUL (nothing) @TechReport{SLWAZHV04, author={Peter Sewell and James J. Leifer and Keith Wansbrough and Mair Allen-Williams and Zappa Nardelli, Francesco and Pierre Habouzit and Viktor Vafeiadis}, title= {Acute: High-level programming language design for distributed computation. Design rationale and language definition}, institution= {University of Cambridge Computer Laboratory}, year={2004}, number={605}, month=oct, note={Also published as INRIA RR-5329. 193pp} } @InProceedings{LNSW04, author={James Leifer and Michael Norrish and Peter  Sewell and Keith Wansbrough}, title={Acute and {TCP}: specifying and developing abstractions for global computation}, booktitle={Proceedings of the APPSEM II Workshop, Tallinn. 2pp}, pages={}, year={2004}, month=apr } @TechReport{BHSSW04-tr, author={Gavin Bierman and Michael Hicks and Peter Sewell and Gareth Stoyle and Keith Wansbrough}, title ={Dynamic Rebinding for Marshalling and Update, with Destruct-time $\lambda$}, institution={University of Cambridge Computer Laboratory}, year={2004}, number={UCAM-CL-TR-568}, month =feb } @InProceedings{lawall:plos04, AUTHOR = {Julia L. Lawall and Anne-Fran\c{c}oise Le Meur and Gilles Muller}, YEAR = {2004}, TITLE = {Modularity for the Bossa Process-Scheduling Language}, BOOKTITLE = {ECOOP Workshop on Programming Languages and Operating Systems (ECOOP-PLOS 2004)}, editor = {}, publisher = {}, organization = {}, address = {Oslo, Norway}, series = {Technical report TR-ICS-04-22, Donald Bren School of Information and Computer Science, University of California, Irvine}, volume = {}, pages = {1--5}, month = {June}, keywords = {}, summary = {Bossa is a framework for implementing scheduling policies in standard operating systems. This frame­work provides a domain-specific language that eases the specification of scheduling policies and enables verification of critical safety properties. In previous work we have specified the semantics of the Bossa language and the verification process. In this work, we propose a modular version of the language, to take advantage of the many opportunities for code reuse and modularity provided by scheduling policies. }, theme = {A}, deliverable = {D13}, site = {copenhagen} } %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%# % FROM genoa.bib %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%# @string{acm="ACM Press"} @string{kl="Kluwer Academic Publishers"}@string{popl04="ACM Symp. on Principles of Programming Languages 2004"} @string{oops04="ACM Symp. on Applied Computing (SAC 2004), Special Track on Object-Oriented Programming Languages and Systems"} @Article{Mog+Sab:AMSVR-03-09, author = {E. Moggi and A. Sabry}, title = {An Abstract Monadic Semantics for Value Recursion}, Journal = {Theoretical Informatics and Applications}, volume=38, year=2004, pdf= {http://www.disi.unige.it/person/MoggiE/ftp/MS03-sub.pdf}, abstract={ This paper proposes an operational semantics for value recursion in the context of monadic metalanguages. Our technique for combining value recursion with computational effects works \emph{uniformly} for all monads. The operational nature of our approach is related to the implementation of recursion in Scheme and its monadic version proposed by Friedman and Sabry, but it defines a different semantics and does not rely on assignments. When contrasted to the axiomatic approach proposed by Erk\"ok and Launchbury, our semantics for the continuation monad invalidates one of the axioms, adding to the evidence that this axiom is problematic in the presence of continuations. }, theme = {A}, workpackage = {2}, site = {genova}} @Article{FagorziZucca04, author = "S. Fagorzi and E. Zucca", title = "A Case-Study in Encoding Configuration Languages: Multiple Class Loaders", journal = "Journal of Object Technology", year = 2004, note = {To appear}, theme = {A}, workpackage = {2}, site = {genova}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%# % FROM inria.bib %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%# @string{lncs = {Lecture Notes in Computer Science}} @string{springer = {Springer-Verlag}} @string{acm = {ACM Press}} @string{jfp = {Journal of Functional Programming}} @string{mscs = {Methematical Structures in Computer Science}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%% Les marroniers (reviennent tous les ans) %%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @Manual{0000-Ocaml-manual, theme = {AE}, workpackage = {1}, site = {inria}, title = {The {Objective} {Caml} system, documentation and user's manual -- release 3.08}, author = {Xavier Leroy and Damien Doligez and Jacques Garrigue and Didier Rémy and Jérôme Vouillon}, organization = {INRIA}, month = jul, year = 2004, url = {http://caml.inria.fr/ocaml/htmlman/} } @inproceedings{2004-Gauthier-Pottier, theme = {AE}, workpackage = {1}, site = {inria}, author = {Nadji Gauthier and François Pottier}, title = {Numbering Matters: First-Order Canonical Forms for Second-Order Recursive Types}, booktitle = {Proceedings of the 2004 {ACM} {SIGPLAN} International Conference on Functional Programming (ICFP'04)}, url ={http://cristal.inria.fr/~fpottier/publis/gauthier-fpottier-icfp04.pdf}, acm = {http://doi.acm.org/10.1145/1016850.1016872}, month = SEP, year = {2004}, pages = {150--161}, abstract = { We study a type system equipped with universal types and equirecursive types, which we refer to as $F_\mu$. We show that type equality may be decided in time $O(n\log n)$, an improvement over the previous known bound of $O(n^2)$. In fact, we show that two more general problems, namely entailment of type equations and type unification, may be decided in time $O(n\log n)$, a new result. To achieve this bound, we associate, with every $F_\mu$ type, a \emph{first-order canonical form}, which may be computed in time $O(n\log n)$. By exploiting this notion, we reduce all three problems to equality and unification of \emph{first-order} recursive terms, for which efficient algorithms are known.} } @article{2004-Hirschowitz-Leroy-TOPLAS, theme = {AE}, workpackage = {1}, site = {inria}, author = "Tom Hirschowitz and Xavier Leroy", title = "Mixin modules in a call-by-value setting", journal = "ACM Transactions on Programming Languages and Systems", year = 2004, URL = {http://cristal.inria.fr/~xleroy/publi/mixins-cbv-toplas.pdf}, note = "Accepted for publication, to appear", abstract = {The ML module system provides powerful parameterization facilities, but lacks the ability to split mutually recursive definitions across modules, and does not provide enough facilities for incremental programming. A promising approach to solve these issues is Ancona and Zucca's mixin modules calculus CMS. However, the straightforward way to adapt it to ML fails, because it allows arbitrary recursive definitions to appear at any time, which ML does not support. In this paper, we enrich CMS with a refined type system that controls recursive definitions through the use of dependency graphs. We then develop a separate compilation scheme, directed by dependency graphs, that translate mixin modules down to a CBV lambda-calculus extended with a non-standard let rec construct}} @inproceedings{2004-Hirschowitz-Leroy-Wells, theme = {AE}, workpackage = {1}, site = {inria}, author = {Tom Hirschowitz and Xavier Leroy and J. B. Wells}, title = {Call-by-Value Mixin Modules: Reduction Semantics, Side Effects, Types}, booktitle = {European Symposium on Programming}, volume = 2986, series = lncs, publisher = springer, pages = "64--78", year = {2004}, url = {http://cristal.inria.fr/~xleroy/publi/mixins-mm-esop2004.ps.gz}, abstract = {Mixin modules are a framework for modular programming that supports code parameterization, incremental programming via late binding and redefinitions, and cross-module recursion. In this paper, we develop a language of mixin modules that supports call-by-value evaluation, and formalize a reduction semantics and a sound type system for this language.} } @unpublished{2004-Hirschowitz-Leroy-Wells-HOSC, theme = {AE}, workpackage = {1}, site = {inria}, author = {Tom Hirschowitz and Xavier Leroy and J. B. Wells}, title = {Compilation of extended recursion in call-by-value functional languages}, month = nov, year = 2004, note = {submitted and resubmitted after revision to \emph{Higher-Order and Symbolic Computation}} } @inproceedings{2004-Hirschowitz-Leroy-Wells-APPSEM, theme = {AE}, workpackage = {1}, site = {inria}, author = {Tom Hirschowitz and Xavier Leroy and J. B. Wells}, title = {Extended recursive definitions in call-by-value languages, with applications to mixin modules and recursive modules}, booktitle = {Electronic proceedings of the second APPSEM II Workshop}, city = {Tallin}, year = {2004}, month = apr } @InCollection{2004-Pottier-Remy-ATTAPL, theme = {AE}, workpackage = {1}, site = {inria}, author = "Fran{\c{c}}ois Pottier and Didier R{\'{e}}my", booktitle = "Advanced Topics in Types and Programming Languages", title = "The Essence of {ML} Type Inference", pages = "389--489", publisher = "MIT Press", year = "2005", editor = "Benjamin C. Pierce", chapter = "10", } @InProceedings{2004-Pottier-Gauthier-POPL, theme = {AE}, workpackage = {1}, site = {inria}, author = "François Pottier and Nadji Gauthier", title = "Polymorphic Typed Defunctionalization", booktitle = "31st ACM symposium on Principles of Programming Languages", publisher = acm, month = jan, year = "2004", pages = "89--98", url ="http://cristal.inria.fr/~fpottier/publis/fpottier-gauthier-popl04.pdf", abstract = {\emph{Defunctionalization} is a program transformation that aims to turn a higher-order functional program into a first-order one, that is, to eliminate the use of functions as first-class values. Its purpose is thus identical to that of \emph{closure conversion}. It differs from closure conversion, however, by storing a \emph{tag}, instead of a code pointer, within every closure. Defunctionalization has been used both as a reasoning tool and as a compilation technique. Defunctionalization is commonly defined and studied in the setting of a simply-typed $\lambda$-calculus, where it is shown that semantics and well-typedness are preserved. It has been observed that, in the setting of a polymorphic type system, such as ML or System F, defunctionalization is not type-preserving. In this paper, we show that extending System F with \emph{guarded algebraic data types} allows recovering type preservation. This result allows adding defunctionalization to the toolbox of type-preserving compiler writers.}, } @Unpublished{2004-Pottier-Regis-Gianas, theme = {ABE}, workpackage = {1}, site = {inria}, author = "François Pottier and Yann {Régis-Gianas}", title = "Towards efficient, typed {LR} parsers", url = "http://cristal.inria.fr/~fpottier/publis/fpottier-regis-gianas-jfp04.pdf", month = sep, year = "2004", abstract = {The LR parser generators that are bundled with many functional programming language implementations produce code that is unsafe, needlessly inefficient, or both. We show that, using generalized algebraic data types, it is possible to produce parsers that are well-typed (so they cannot unexpectedly crash or fail) and nevertheless efficient. This is a useful result as well as a nice exercise in programming with generalized algebraic data types.}, note = "Submitted to the \emph{Journal of Functional Programming}", } @PhdThesis{2004-Pottier-hdr, author = "François Pottier", title = "Types et contraintes", school = "Université Paris 7", month = dec, type = "Mémoire d'habilitation à diriger des recherches", year = "2004", url = "http://cristal.inria.fr/~fpottier/publis/fpottier-hdr.pdf" } @Unpublished{2004-Simonet-Pottier-hmg, author = "Vincent Simonet and François Pottier", title = "Constraint-Based Type Inference with Guarded Algebraic Data Types", note = "Submitted to \emph{ACM Transactions on Programming Languages and Systems}", month = jun, year = "2004", URL = "http://cristal.inria.fr/~fpottier/publis/simonet-pottier-hmg.pdf", } @PhdThesis{2004-Simonet-these, author = {Vincent Simonet}, TITLE = {Inférence de flots d'information pour {ML}: formalisation et implantation}, school = {Université Paris 7}, year = 2004, month = mar, URL = {http://cristal.inria.fr/~simonet/publis/simonet-these.pdf}, ABSTRACT = {This thesis describes the conception of an information flow analyser for a language of the ML family, from its theoretical foundation to the practical issues. The first part of the dissertation presents the tool that was implemented, Flow Caml, and illustrates its use on concrete example. The second part gives a formalization of the type system featured by Flow Caml, together with a proof of its correctness. This is the first type system for information flow analysis in a realistic programming language that has been formally proved. Lastly, the third part is devoted to the formalization and the proof of an efficient algorithm for type inference in the presence of structural subtyping and polymorphism. An instance of this algorithm is used to synthesize types in Flow Caml.} } @PhdThesis{2004-LeBotlan-these, author = {{Le Botlan}, Didier}, title = {{MLF}: Une extension de {ML} avec polymorphisme de second ordre et instanciation implicite.}, school = {École Polytechnique}, year = 2004, month = may, URL = "http://www.inria.fr/rrrt/tu-1071.html", abstract = { Nous nous intéressons à une extension de ML avec polymorphisme de première classe, à la manière du Système~{F}. Cette extension, nommée {MLF}, utilise les annotations de types d'ordre supérieur données explicitement dans le programme pour inférer de manière principale le type le plus général. Toute expression admet ainsi un type principal, qui dépend des annotations présentes initialement dans le programme. \par Toute expression de {ML} est typable dans {MLF} sans annotation supplémentaire. Les expressions du Système {F} sont encodées de manière systématique dans {MLF} en supprimant les abstractions et les applications de types, et en traduisant les annotations de types dans le langage de types de {MLF}. De plus, les paramètres de lambda-abstractions qui ne sont pas utilisés de manière polymorphe n'ont pas besoin d'être annotés. }} @InProceedings{2004-Yakobowski-LOPSTR, author = {J. B. Wells and Boris Yakobowski}, title = {Graph-Based Proof Counting and Enumeration with Applications for Program Fragment Synthesis}, pdf = {http://www.yakobowski.org/content/term-enumeration-final.pdf}, abstract = {For use in earlier approaches to automated module interface adaptation, we seek a restricted form of program synthesis. Given some typing assumptions and a desired result type, we wish to automatically build a number of program fragments of this chosen typing, using functions and values available in the given typing environment. We call this problem \emph{term enumeration}. To solve the problem, we use the Curry-Howard correspondence (propositions-as-types, proofs-as-programs) to transform it into a \emph{proof enumeration} problem for an intuitionistic logic calculus. We formally study proof enumeration and counting in this calculus. We prove that proof counting is solvable and give an algorithm to solve it. This in turn yields a proof enumeration algorithm.}, year = 2004, key = {LO{\relax PSTR} '04}, booktitle = {International Symposium on Logic-based Program Synthesis and Transformation 2004 (LOPSTR 2004)}, editor = {Sandro Etalle}, volume = {3049}, series = LNCS, publisher = Springer } % xaddress = {Verona, Italy}, @MastersThesis{2004-Yakobowski-DEA, author = {Boris Yakobowski}, title = {Étude sémantique d'un langage intermédiaire de type Static Single Assignment}, type = {{Master's} dissertation (mémoire de stage de {DEA})}, school = {ENS Cachan}, year = {2004}, month = sep, } %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%% INRIA RENNES %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @Article{Besson:05:Interfaces, author = "Fr\'ed\'eric Besson and Thomas de Grenier de Latour and Thomas Jensen", title = "Interfaces for stack inspection", journal = "Journal of Functional Programming", note = "To appear", year = {2005}, site = {inria}, workpackage = {1}, theme = {ACDE} } @InProceedings{CachJen:esop04, author = {David Cachera and Thomas Jensen and David Pichardie and Vlad Rusu}, title = {Extracting a data flow analyser in constructive logic}, booktitle = "Proc.~ESOP'04", series = "Springer LNCS", number = "2986", pages = "385 -- 400", year = "2004", note = "Extended version to appear in TCS", site = {inria}, theme = {BCD} } %THEME A @Misc{LS-04b, author = {L. Liquori and A.Spiwack}, title = {{Inferring Types for Functional Methods}}, howpublished = {Manuscript}, year = {2004}, workpackage = {1}, site = {Loria}, theme={A}, note = {\url{http://www.sop-inria.fr/mirho/Luigi.Liquori/PAPERS/t41.ps.gz}} } @Misc{LS-04a, author = {L. Liquori and A.Spiwack}, title = {{Featherweight-Trait Java, A Trait-based Extension for FJ}}, howpublished = {Manuscript}, year = {2004}, workpackage = {1}, site = {Loria}, theme={A}, note = {\url{http://www.sop-inria.fr/mirho/Luigi.Liquori/PAPERS/ftj.ps.gz}} } @Misc{FL-04, author = {S. Fechter and L. Liquori}, title = {{Mini-Foc: A Kernel Calculus for Certified Computer Algebra [Ongoing Work]}}, howpublished = {Manuscript}, year = {2004}, workpackage = {1}, site = {Loria}, theme={A}, note = {\url{http://www.sop-inria.fr/mirho/Luigi.Liquori/PAPERS/minifoc.ps.gz}} } @Article{CLM-04, author = {A. Ciaffaglione and L. Liquori and M. Miculan}, title = {{Reasoning about Calculi of Objects in (Co)Inductive Type Theories with the Theory of Contexts}}, journal = {Journal of Automated Reasoning}, year = {200X}, publisher = {Kluwer}, workpackage = {1}, site = {Loria}, volume = {}, number = {}, theme={A}, note = {Under Major Revision, \url{http://www.sop-inria.fr/mirho/Luigi.Liquori/PAPERS/jar-04.ps.gz}} } @InProceedings{DLLL-04, author = {D. Dougherty and P. Lescanne and L. Liquori and F. Lang}, title = {{Addressed Term Rewriting Systems: Syntax, Semantics, and Pragmatics [Extended Abstract]}}, booktitle = {Proc. of TERMGRAPH, International Workshop on Term Graph Rewriting}, year = {2004}, series = {ENTCS}, publisher = {Elsevier}, number = {To appear}, workpackage = {1}, site = {Loria}, theme={A}, note = { \url{http://www.sop-inria.fr/mirho/Luigi.Liquori/PAPERS/termgraph-04.ps.gz}} } @inproceedings{ghani-wood04, theme = {A}, site = {leicester}, author = {Neil Ghani and Johan Glimming}, title = {{Difunctorial Semantics of Object Calculus}}, booktitle = {Electronic Notes in Theoretical Computer Science}, volume = {To Appear}, issue = {}, publisher = {Elsevier Science Publishers}, editor = {}, year = {2004} } @article{ghani-tia04, theme = {C}, site = {leicester}, author = {Neil Ghani and Tarmo Uustalu}, title = {{Coproducts of Ideal Monads}}, journal = {Journal of Theoretical Informatics and Applications}, number = {38}, pages = {321-342}, year = {2004} } @inproceedings{1028990, author = {Bruno Dufour and Christopher Goard and Laurie Hendren and Oege de Moor and Ganesh Sittampalam and Clark Verbrugge}, title = {Measuring the dynamic behaviour of {AspectJ} programs}, booktitle = {Proceedings of the 19th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications}, year = {2004}, isbn = {1-58113-831-9}, pages = {150--169}, location = {Vancouver, BC, Canada}, doi = {http://doi.acm.org/10.1145/1028976.1028990}, publisher = {ACM Press}, } @techreport{aosd05abc, author = "Pavel Avgustinov and Aske Simon Christensen and Laurie Hendren and Sascha Kuzins and Jennifer Lhot{\'{a}}k and Ondrej Lhot{\'{a}}k and Oege de Moor and Damien Sereni and Ganesh Sittampalam and Julian Tibble", title = "{\em abc}: An Extensible {AspectJ} Compiler", institution = "aspectbench.org", number = "abc-2004-1", year = "2004", note = "Accepted for publication at AOSD 2005"} @techreport{cc05abc, author = "Pavel Avgustinov and Aske Simon Christensen and Laurie Hendren and Sascha Kuzins and Jennifer Lhot{\'{a}}k and Ondrej Lhot{\'{a}}k and Oege de Moor and Damien Sereni and Ganesh Sittampalam and Julian Tibble", title = "Building the {\em abc} {AspectJ} compiler with {P}olyglot and {S}oot", institution = "aspectbench.org", number = "abc-2004-2", year = "2004", note = "Submitted to CC 2005"} @STRING{PROC = "Proc. of "} @STRING{MSCS = "Mathematical Structures in Computer Science"} @string{IC = "Information and Computation"} @string{FOSSACS = "Foundations of Software Science and Computation Structures (FOSSACS)"} @STRING{ICFP = "ACM International Conference on Functional Programming (ICFP)"} @STRING{LRPP= "Workshop on Logics for Resources, Processes, and Programs (LRPP)"} @STRING{FSTTCS= "Foundations of Software Technology and Theoretical Computer Science (FSTTCS)"} @STRING{PLANX = "Workshop on Programming Language Technologies for XML (PLAN-X)"} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%# @inproceedings{BB04sblp, title = "Towards a Relational Model for Component Interconnection", author = "Barbosa, M. A. and Barbosa, L. S.", booktitle = "Proc. 8th Brazilian Symposium on Programming Languages", pages = "17--30", editor = "Lins, R. and Braga, C. and Chalub, F.", year = 2004, month = "May", address = "Niteroi, Brasil" } @inproceedings{MB04, author = "Sun M., and Barbosa, L. S.", title = "On Refinement of Generic Software Components", booktitle = "10th Int. Conf. Algebraic Methods and Software Technology ({AMAST})", editor = "Rettray, C. and Maharaj, S. and Shankland, C.", address = "Stirling", pages = "506--520", month = "August", publisher = "Springer Lect. Notes Comp. Sci. (3116)", year = 2004, note = "Best Student Co-authored Paper Award" } @inproceedings{SABZ04, author = "Sun M., and Aichernig, B. K. and Barbosa, L. S. and Naixiao, Z.", title = "A Coalgebraic Semantic Framework for Component Based Development in {UML}", booktitle = "Proc. Int. Conf. on Category Theory and Computer Science (CTCS'04)", editor = "Birkedal, L.", publisher = "{ENTCS} (to appear), Elsevier", month = "August", year = 2004 } @inproceedings{SZB04, author = "Sun M., and Naixiao, Z. and Barbosa, L. S.", title = "On Semantics and Refinement of {UML} Statecharts: A Coalgebraic View", booktitle = "Proc. of 2nd IEEE Int. Conf. on Software Engineering and Formal Methods", publisher = "IEEE Computer Society Press", pages = "164--173", editor = "Cuellar, J. and Liu, Z.", address = "Beijing, China", month = "September", year = 2004 } @inproceedings{BB04ictac, author = "Barbosa, M. A. and Barbosa, L. S.", title = "Specifying Software Connectors", booktitle = "1st International Colloquium on Theorectical Aspects of Computing ({ICTAC'04})", editor = "Araki, K. and Liu, Z.", address = "Guiyang, China", month = "September", publisher = "Springer Lect. Notes Comp. Sci. (to appear)", year = 2004 } @inproceedings{RB04, author = "Rodrigues, N. and Barbosa, L. S.", title = "Prototyping Behavioural Specifications in the {.Net} Framework", booktitle = "Proc. 7th Brazilian Symposium on Formal Methods (SBMF'2004)", publisher = "{ENTCS} (to appear), Elsevier", month = "November", year = 2004 } % ---- Thesis @PhdThesis{mjf:phd, author = {Maria Jo\~{a}o Frade}, title = {Type-Based Termination of Recursive Definitions and Constructor Subtyping in Typed Lambda Calculi}, school = {Universidade do Minho}, year = {2004} } @InProceedings{AnconaZucca04, author = "D. Ancona and E. Zucca", title = "Principal Typings for {J}ava-like languages", booktitle=popl04, month = {January}, year=2004, publisher = acm, pages ={306--317}, theme = {E}, workpackage = {1}, site = {genova}} % aarhus-2005.bib @STRING{LNCS = "Lecture Notes in Computer Science"} @STRING{MFPS = "Mathematical Foundations of Programming Semantics"} @STRING{MFPS05 = "Proceedings of the 21st Conference on the " # MFPS} @PhDThesis{Ager:PhD, author = "Mads Sig Ager", title = "Partial Evaluation of String Matchers \& Constructions of Abstract Machines", school = "BRICS PhD School, University of Aarhus", address = "Aarhus, Denmark", year = 2006, month = Jan, package = 3, theme = "B, C, and F", site = "Aarhus" } @Article{Ager-al:TOPLAS??, author = "Mads Sig Ager and Olivier Danvy and Henning Korsholm Rohde", title = "Fast Partial Evaluation of Pattern Matching in Strings", journal = "ACM Transactions on Programming Languages and Systems", year = 2006, OPTvolume = ?, OPTnumber = ?, OPTpages = "?-?", note = "To appear. Available as the technical report BRICS RS-04-40. A preliminary version was presented at the 2003 {ACM} {SIGPLAN} Workshop on Partial Evaluation and Semantics-Based Program Manipulation (PEPM 2003)", package = 3, theme = "C", site = "Aarhus" } @Article{Ager-al:IPL04, author = "Mads Sig Ager and Olivier Danvy and Jan Midtgaard", title = "A Functional Correspondence between Call-by-Need Evaluators and Lazy Abstract Machines", journal = "Information Processing Letters", year = 2004, pages = "223-232", volume = 90, number = 5, note = "Extended version available as the technical report BRICS RS-04-3", package = 3, theme = "F", site = "Aarhus" } @Article{Ager-al:TCS05, author = "Mads Sig Ager and Olivier Danvy and Jan Midtgaard", title = "A Functional Correspondence between Monadic Evaluators and Abstract Machines for Languages with Computational Effects", journal = "Theoretical Computer Science", year = 2005, volume = 342, number = 1, pages = "149-172", note = "Extended version available as the technical report BRICS RS-04-28", package = 3, theme = "F", site = "Aarhus" } @PhDThesis{Biernacka:PhD, author = "Ma{\l}gorzata Biernacka", title = "A Derivational Approach to the Operational Semantics of Functional Languages", school = "BRICS PhD School, University of Aarhus", address = "Aarhus, Denmark", year = 2006, month = Jan, package = 3, theme = "B, C, and F", site = "Aarhus" } @InProceedings{Biernacka-al:MFPS05, author = "Ma{\l}gorzata Biernacka and Olivier Danvy and Kristian Støvring", OPTtitle = "Extracting evaluators from proofs of weak head normalization", title = "Program extraction from proofs of weak head normalization", crossref = "MFPS:05", OPTpages = "25-33", note = "Extended version available as the technical report BRICS RS-05-12", package = 3, theme = "B", site = "Aarhus" } @Article{Biernacka-al:LMCS05, author = "Ma{\l}gorzata Biernacka and Dariusz Biernacki and Olivier Danvy", title = "An Operational Foundation for Delimited Continuations in the {CPS} Hierarchy", journal = "Logical Methods in Computer Science", year = 2005, month = Nov, volume = 1, number = "2:5", pages = "1-39", note = "A preliminary version was presented at the Fourth ACM SIGPLAN Workshop on Continuations (CW'04)", package = 3, theme = "F", site = "Aarhus" } @Article{Biernacka-Danvy:TOCL06, author = "Ma{\l}gorzata Biernacka and Olivier Danvy", title = "A Concrete Framework for Environment Machines", journal = "ACM Transactions on Computational Logic", year = 2006, OPTvolume = ?, OPTnumber = ?, OPTpages = "?-?", note = "To appear. Available as the technical report BRICS RS-06-3", package = 3, theme = "F", site = "Aarhus" } @TechReport{Biernacka-Danvy:RS-05-38, author = "Ma{\l}gorzata Biernacka and Olivier Danvy", title = "A Syntactic Correspondence between Context-Sensitive Calculi and Abstract Machines", institution = "DAIMI, Department of Computer Science, University of Aarhus", year = 2005, type = "Technical Report", number = "BRICS RS-05-38", address = "Aarhus, Denmark", month = Dec, note = "Accepted for publication in Theoretical Computer Science (March 2006)", package = 3, theme = "F", site = "Aarhus" } @PhDThesis{Biernacki:PhD, author = "Dariusz Biernacki", title = "The Theory and Practice of Programming Languages with Delimited Continuations", school = "BRICS PhD School, University of Aarhus", address = "Aarhus, Denmark", year = 2005, month = Dec, package = 3, theme = "B, C, and F", site = "Aarhus" } @Article{Biernacki-al:IPL05, author = "Dariusz Biernacki and Olivier Danvy and {Chung-chieh} Shan", title = "On the Dynamic Extent of Delimited Continuations", journal = "Information Processing Letters", year = 2005, volume = 96, number = 1, pages = "7-17", package = 3, theme = "B", site = "Aarhus" } @Article{Biernacki-al:SCP06, author = "Dariusz Biernacki and Olivier Danvy and {Chung-chieh} Shan", title = "On the Static and Dynamic Extents of Delimited Continuations", journal = "Science of Computer Programming", year = 2006, OPTvolume = ?, OPTnumber = ?, OPTpages = "?-?", note = "To appear. Available as the technical report BRICS RS-05-36", package = 3, theme = "B", site = "Aarhus" } @Article{Biernacki-Danvy:JFP06, author = "Dariusz Biernacki and Olivier Danvy", title = "A Simple Proof of a Folklore Theorem about Delimited Control", journal = "Journal of Functional Programming", year = 2006, OPTvolume = ?, OPTnumber = ?, OPTpages = "?-?", note = "To appear. Available as the technical report BRICS RS-05-25", package = 3, theme = "B", site = "Aarhus" } @InProceedings{Danvy:IFL04, author = "Olivier Danvy", title = "A Rational Deconstruction of {L}andin's {SECD} Machine", crossref = "IFL:04", pages = "52-71", note = "Recipient of the 2004 Peter Landin prize. Extended version available as the technical report BRICS RS-03-33", package = 3, theme = "F", site = "Aarhus" } @Article{Danvy-Goldberg:FI05, author = "Olivier Danvy and Mayer Goldberg", title = "There and back again", journal = "Fundamenta Informaticae", year = 2005, volume = 66, number = 4, pages = "397-413", note = "A preliminary version was presented at the 2002 {ACM} {SIGPLAN} International Conference on Functional Programming (ICFP 2002)", package = 3, theme = "F", site = "Aarhus" } @InProceedings{Danvy-Millikin:IFL05, author = "Olivier Danvy and Kevin Millikin", title = "A Rational Deconstruction of {L}andin's {J} Operator", crossref = "IFL:05", OPTpages = "?-?", note = "To appear. Extended version available as the technical report BRICS RS-06-4 (February 2006)", package = 3, theme = "F", site = "Aarhus" } @Article{Danvy-Nielsen:IPL05, author = "Olivier Danvy and Lasse R. Nielsen", title = "{CPS} Transformation of Beta-Redexes", journal = "Information Processing Letters", year = 2005, volume = 94, number = 5, pages = "217-224", note = "Extended version available as the research report BRICS RS-04-39", package = 3, theme = "C", site = "Aarhus" } @Article{Danvy-Rohde:IPL06, author = "Olivier Danvy and Henning Korsholm Rohde", title = "On Obtaining the {B}oyer-{M}oore String-Matching Algorithm by Partial Evaluation", journal = "Information Processing Letters", year = 2006, OPTvolume = ?, OPTnumber = ?, OPTpages = "?-?", note = "To appear. Available as the technical report BRICS RS-05-29", package = 3, theme = "C", site = "Aarhus" } @Article{Danvy-Schultz:JFLP04, author = "Olivier Danvy and Ulrik P. Schultz", title = "Lambda-Lifting in Quadratic Time", journal = "Journal of Functional and Logic Programming", volume = 10, number = 1, OPTpages = "?", month = Jul, year = 2004, note = "Available online at \url{http://danae.uni-muenster.de/lehre/kuchen/JFLP/}. A preliminary version was presented at the Sixth International Symposium on Functional and Logic Programming (FLOPS 2002)", package = 3, theme = "C", site = "Aarhus" } @Article{Filinski-Rohde:RAIRO05, author = "Andrzej Filinski and Henning Korsholm Rohde", title = "Denotational Aspects of Untyped Normalization by Evaluation", journal = "Theoretical Informatics and Applications", year = 2005, volume = 39, number = 3, pages = "423-453", theme = "C", site = "Copenhagen and Aarhus" } @PhDThesis{Rohde:PhD, author = "Henning Korsholm Rohde", title = "Formal Aspects of Partial Evaluation", school = "BRICS PhD School, University of Aarhus", address = "Aarhus, Denmark", year = 2005, month = Dec, package = 3, theme = "B, C", site = "Aarhus" } @Proceedings{IFL:04, key = "Grelck et al.", title = "Implementation and Application of Functional Languages, 16th International Workshop, IFL'04", booktitle = "Implementation and Application of Functional Languages, 16th International Workshop, IFL'04", editor = "Clemens Grelck and Frank Huch and Greg J. Michaelson and Phil Trinder", series = LNCS, number = 3474, publisher = "Springer", address = "Lübeck, Germany", month = Sep, year = 2004, OPTnote = "Revised Selected Papers" } @Proceedings{IFL:05, key = "Michaelson", title = "Implementation and Application of Functional Languages, 17th International Workshop, IFL'05", booktitle = "Implementation and Application of Functional Languages, 17th International Workshop, IFL'05", editor = "Greg J. Michaelson", series = LNCS, OPTnumber = "?", publisher = "Springer", address = "Dublin, Ireland", month = Sep, year = 2005, OPTnote = "Revised Selected Papers" } @Proceedings{MFPS:05, key = "Escard\'o", title = MFPS05, year = 2005, booktitle = MFPS05, series = "Electronic Notes in Theoretical Computer Science", OPTvolume = 45, editor = "Martin Escard\'o", publisher = "Elsevier Science Publishers", address = "Birmingham, UK", month = May, note = "To appear" } @InProceedings{escardo:ho, author = {M.H. Escard\'o and W.K. Ho}, title = {Operational domain theory and topology of a sequential programming language}, booktitle = {Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science}, pages = {427--436}, year = 2005, publisher = {IEEE Computer Society}, theme = {D,I} } @Article{escardo:ccg, author = {M.H. Escard\'o}, title = {Compactly generated {H}ausdorff locales}, journal = {Annals of Pure and Applied Logic}, year = 2005, volume = 137, number = {1--3}, pages = {147--163}, theme = {D,I} } @Article{Ritter:apcs05, author = {V. de Paiva and P. Maneggia and M. Maietti and E. Ritter}, title = {Relating categorical semantics for intuitionistic linear logic}, journal = {Applied Categorical Structures}, year = 2005, volume = 13, pages = {1--36}, theme = {C} } @InProceedings{Ritter:FC05, author = {S. Kremer and A. Mukhamedov and E. Ritter}, title = {Analysis of a multi-party fair exchange protocol and formal proof of correctness in the strand space model}, booktitle = {Proceedings of the 2005 Conference on Financial Cryptography and Data Security}, pages = {255--269}, year = 2005, editor = {A. S. Patrick and M. Yung}, series = {Lecture Notes in Computer Science}, publisher = {Springer Verlag}, theme = {D} } @inproceedings{DBLP:conf/popl/Ghica05, author = {Dan R. Ghica}, title = {Slot games: a quantitative model of computation.}, booktitle = {POPL}, year = {2005}, pages = {85-97}, ee = {http://doi.acm.org/10.1145/1040305.1040313}, crossref = {DBLP:conf/popl/2005}, bibsource = {DBLP, http://dblp.uni-trier.de}, theme = {F} } @inproceedings{DBLP:conf/sas/DimovskiGL05, author = {Aleksandar Dimovski and Dan R. Ghica and Ranko Lazic}, title = {Data-Abstraction Refinement: A Game Semantic Approach.}, booktitle = {SAS}, year = {2005}, pages = {102-117}, ee = {http://dx.doi.org/10.1007/11547662_9}, crossref = {DBLP:conf/sas/2005}, bibsource = {DBLP, http://dblp.uni-trier.de}, theme = {F} } @Article{Levy:adjunctionsjourn, author = {P. B. Levy}, title = {Adjunction Models For Call-By-Push-Value With Stacks}, journal = {Theory and Applications of Categories}, year = {2005}, volume = {14}, theme = {F,G} } @TechReport{zawawy70, author = {M. A. El-Zawawy and A. Jung}, title = {A Priestley representation for strong proximity lattices and stably compact spaces}, institution = {University of Birmingham, School of Computer Science}, number = {CSR-05-3}, year = 2005, url = {ftp://ftp.cs.bham.ac.uk/pub/tech-reports/2005/CSRP-05-03.ps.gz}, theme = {I} } @InProceedings{Schwinghammer:05, author = {Jan Schwinghammer}, title = {A Typed Semantics of Higher-Order Store and Subtyping}, booktitle = {Proceedings Ninth Italian Conference on Theoretical Computer Science}, year = 2005, series = {Lecture Notes in Computer Science}, publisher = {Springer}, volume = {3701}, editor = {Mario Coppo, Elena Lodi, G. Michele Pinna}, pages = {390--404}, } @PhdThesis{Schwinghammer:Diss, author = {Jan Schwinghammer}, title = {Reasoning about Denotations of Recursive Objects}, school = {University of Sussex}, year = 2005, note = {Submitted in Sept.\ 2005} } @INPROCEEDINGS{ReusStreicher:ICALP, author = {B. Reus and Th. Streicher}, title = {About Hoare Logics for Higher-order Store}, booktitle = {Proceedings of the 32th Intern.\ Conference on Automata, Languages, and Programming Languages}, year = {2005}, series = {LNCS}, editor = {Lu\'is Caires and Giuseppe F. Italiano and Lu\'is Monteiro and Catuscia Palamidessi and Moti Yung}, volume = {3580}, pages = {1337--1348} } @InProceedings{Reus:Schwinghammer:05, author = {B. Reus and J. Schwinghammer}, title = {Denotational Semantics for {Abadi} and {Leino}'s Logic of Objects}, booktitle = {European Symposium on Programming}, year = {2005}, editor = {Mooly Sagiv}, pages = {263--278}, volume = {3444}, series = {Lecture Notes in Computer Science}, publisher = {Springer Verlag} } @inproceedings{PattinsonReus:2005, author = {Dirk Pattinson and Bernhard Reus}, title = {A Complete Temporal and Spatial Logic for Distributed Systems}, editors = {Bernhard Gramlich}, booktitle = {Frontiers of Combining Systems (FroCoS)}, series = {Lecture Notes in Artificial Intelligence}, volume = {3717}, year = {2005}, pages = {122--137}, publisher = {Springer-Verlag}, address = {Berlin} } @article{laird-linlong, author = {J. Laird}, title = {Game Semantics and {L}inear {CPS} Interpretation}, journal = {Theoretical Computer Science}, volume = {333}, pages = {199--224}, publisher = {Elsevier}, year = 2005} @article{laird-fi05, author = {J. Laird}, title = {Sequentiality in Bounded Bidomains}, journal = {Fundamenta Informaticae}, volume = 65, pages = {173 -- 191}, publisher = {IOS press}, year = 2005} @article{laird-LBD, author = {J. Laird}, title = {Locally Boolean Domains}, Journal = {Theoretical Computer Science}, volume = 342, pages = {132 --148}, publisher = {Elsevier}, year = 2005} @inproceedings{laird-tlca05, author = {J. Laird}, title = {The Elimination of Nesting in {SPCF}}, booktitle = {Proceedings of TLCA '05}, publisher = {Springer Verlag}, series = {LNCS}, number = 3461, pages = {234-245}, year = 2005} @inproceedings{laird-icalp05, author = {J. Laird}, title = {Decidability in Syntactic Control of Interference}, booktitle = {Proceedings of ICALP '05}, publisher = {Springer Verlag}, series = {LNCS}, number = 3580, pages = {904-916}, year = 2005} @inproceedings{laird-concur05, author = {J. Laird}, title = {A Game Semantics of the asynchronous pi-calculus}, booktitle = {Proceedings of CONCUR '05}, publisher = {Springer Verlag}, series = {LNCS}, number = 3653, pages = {51--65}, year = 2005 } @article{JR05-famtsco, author = {Jeffrey, Alan and Rathke, Julian}, title = {A fully abstract may testing semantics for concurrent objects}, journal = {Theoretical Computer Science}, year = {2005}, publisher = {Elsevier}, volume = {338}, pages = {17--63}, } @inproceedings{JR05-jjfatscjl, author = {Jeffrey, Alan and Rathke, Julian}, editor = {Sagiv, Mooly}, title = {Java Jr. : Fully abstract trace semantics for a Core Java Language}, year = {2005}, series = {Lecture Notes in Computer Science}, volume = {3444}, publisher = {Springer-Verlag}, pages = {423--438}, } @article{JR05-cehopcr, author = {Jeffrey, Alan and Rathke, Julian}, title = {Contextual equivalence for higher-order pi-calculus revisited}, year = {2005}, journal = {Logical Methods in Computer Science}, publisher = {LMCS-Online}, volume = {1(1:4)}, } @inproceedings{JR05-fappc, author = {Jeffrey, Alan and Rathke, Julian}, editor = {Sassone, Vladimiro}, title = {Full abstraction for Polymorphic Pi-Calculus}, year = {2005}, series = {Lecture Notes in Computer Science}, volume = {3441}, publisher = {Springer-Verlag}, pages = {266--281}, } % General abbreviations @String{ ieee = "IEEE Computer Society Press" } @String{ lncs = "Lecture Notes in Computer Science" } @String{ lnai = "Lecture Notes in Artificial Intelligence" } @String{ entcs = "Electronic Notes in Theoretical Computer Science" } @String{ springer = "Springer" } @String{ tcs = "Theoretical Computer Science" } @STRING{tlca05 = "Typed Lambda Calculi and Applications (TLCA 2005), Nara, Japan" } %%% Theme B %%% @InProceedings{abelBenkeBoveHughesNorell:haskell05, author = {Andreas Abel and Marcin Benke and Ana Bove and John Hughes and Ulf Norell}, title = {Verifying {Haskell} Programs Using Constructive Type Theory}, booktitle = {ACM SIGPLAN Workshop Haskell'05, Tallinn, Estonia, 30 September, 2005}, publisher = {ACM}, year = 2005 } @InProceedings{ abelCoquandNorell:frocos05, author = {Andreas Abel and Thierry Coquand and Ulf Norell}, title = {Connecting a Logical Framework to a First-Order Logic Prover}, booktitle = {5th International Workshop on Frontiers of Combining Systems, FroCoS'05, Vienna, Austria, September 19--21, 2005}, key = {DOI: 10.1007/11559306_17}, pages = {285--301}, year = 2005, editor = {Bernhard Gramlich}, volume = 3717, series = lnai, month = sep, publisher = springer, url = {http://springerlink.metapress.com/link.asp?ID=0LM501YURQXDXL8Y} } @Article{dybjer:jlap, author = {Peter Dybjer and Anton Setzer}, title = {Indexed Induction-Recursion}, journal = {Journal of Logic and Algebraic Programming}, year = 2005, note = {In press} } @inproceedings{coquand:spiwack, AUTHOR = {T. Coquand and A. Spiwack}, TITLE = {Proof of strong normalisation using domain theory}, BOOKTITLE = {{Proceedings of LICS 2006}}, YEAR = {2006} } @PhdThesis{gonzalia:phd, author = {Carlos Gonzalia}, title = {Relations in Dependent Type Theory}, school = {Chalmers University of Technology}, year = 2006 } @InProceedings{abelCoquand:tlca05, author = {Andreas Abel and Thierry Coquand}, title = {Untyped Algorithmic Equality for {Martin-Löf's} Logical Framework with Surjective Pairs}, booktitle = tlca05, key = {DOI: 10.1007/11417170_4}, pages = {23--38}, year = 2005, editor = {Pawe\l{} Urzyczyn}, volume = 3461, series = lncs, month = apr, publisher = springer, url = {http://www.springerlink.com/index/10.1007/11417170_4} } %% Theme D @InProceedings{danielssonetal06:fastandloose, author = {Nils Anders Danielsson and Jeremy Gibbons and John Hughes and Patrik Jansson}, title = {Fast and Loose Reasoning is Morally Correct}, booktitle = {Proceedings of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages}, year = {2006}, note = {Accepted for publication}, url = {http://www.cs.chalmers.se/~nad/publications/danielsson-et-al-popl2006.html} } @InProceedings{danielssonjansson04:chasingbottoms, author = {Nils Anders Danielsson and Patrik Jansson}, title = {Chasing Bottoms, A Case Study in Program Verification in the Presence of Partial and Infinite Values}, booktitle = {Proceedings of the 7th International Conference on Mathematics of Program Construction, {MPC} 2004}, pages = {85--109}, year = {2004}, editor = {Dexter Kozen}, volume = {3125}, series = {{LNCS}}, month = jul, publisher = {Springer-Verlag}, url = {http://www.cs.chalmers.se/~nad/publications/danielsson-jansson-mpc2004.html}} @article{gruenhagestreicher:05, journal = {MSCS}, volume = {to appear in \emph{Keimel Festschrift}}, title = {Quotients of countably based spaces are not closed under sobrification}, author = {Gruenhage, Gary and Streicher, Thomas}, year = 2005 } @inproceedings{reusstreicher:05, volume = 3580, title = {About Hoare logics for higher-order store}, booktitle = {ICALP'05}, year = 2005, pages = { 1337--1348}, publisher = {Springer Verlag}, series = {Lecture Notes in Computer Science}, author = {Reus, Bernhard and Streicher, Thomas} } @article{Keimellawson:05, journal = {{Topology and its Applications}}, volume = 149, title = {Measure extension theorems for $T_0$-spaces}, author = {Keimel, Klaus and Lawson, Jimmie D.}, year = 2005, pages = {57--83}, } @article{tkp:05, journal = {{Electronic Notes in Theoretical Computer Science}}, volume = 129, title = {Semantic Domains for Combining Probability and Non-Determinism}, author = {Tix, Regina and Keimel, Klaus and Plotkin, Gordon D.}, year = 2005, pages = {1--104} } % --------- % Year 2005 % @InProceedings{SereniJones:05:hot, AUTHOR = {Damien Sereni and Neil D. Jones}, YEAR = {2005}, TITLE = {Termination Analysis of Higher-Order Functional Programs}, BOOKTITLE = {Proceedings of the Third Asian Symposium on Programming Languages and Systems (APLAS 2005)}, volume = {3780}, pages = {281--297}, series = {Lecture Notes in Computer Science}, publisher = {Springer-Verlag}, theme = {C}, site = {copenhagen,oxford} } @InProceedings{Lawall:ifm05, AUTHOR = {Jean-Paul Bodeveix and Mamoun Filali and Julia Lawall and Gilles Muller}, YEAR = {2005}, TITLE = {Formal methods meet Domain Specific Languages}, BOOKTITLE = {Fifth International Conference on Integrated Formal Methods}, address = {Eindhoven, The Netherlands}, series = {Lecture Notes in Computer Science}, volume = {3771}, pages = {187--206}, month = nov, theme = {C,D}, site = {copenhagen} } @InProceedings{KawabeGlueck:05:LRS, AUTHOR = {Kawabe, Masahiko and Glück, Robert}, YEAR = {2005}, TITLE = {The Program Inverter {LRinv} and its Structure}, BOOKTITLE = {Practical Aspects of Declarative Languages. Proceedings}, editor = {Hermenegildo, M and Cabeza, D}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {3350}, pages = {219--234}, theme = {C}, site = {copenhagen} } @InProceedings{Lawall:2005:ACP4IS, AUTHOR = {Julia L. Lawall and Gilles Muller and Richard Urunuela}, YEAR = {2005}, TITLE = {Tarantula: Killing Driver Bugs Before They Hatch}, BOOKTITLE = {Proceedings of the Fourth AOSD Workshop on Aspects, Components, and Patterns for Infrastructure Software (ACP4IS)}, address = {Chicago, Illinois}, pages = {13-18}, theme = {C}, site = {copenhagen} } @Article{Filinski-Rohde:RAIRO05, author = {Andrzej Filinski and Henning Korsholm Rohde}, title = {Denotational Aspects of Untyped Normalization by Evaluation}, journal = {Theoretical Informatics and Applications}, year = 2005, volume = 39, number = 3, pages = {423-453}, theme = {C}, site = {copenhagen} } @Article{GlueckKawabe:05:KEinv, AUTHOR = {Glück, Robert and Kawabe, Masahiko}, YEAR = {2005}, TITLE = {Revisiting an Automatic Program Inverter for {Lisp}}, JOURNAL = {SIGPLAN Notices}, volume = {40}, number = {5}, pages = {8--17}, theme = {C}, site = {copenhagen} } @InProceedings{KristiansenJones:05:DataComplexity, AUTHOR = {Kristiansen,Lars and Jones, Neil D.}, YEAR = {2005}, TITLE = {The Flow of Data and the Complexity of Algorithms}, BOOKTITLE = {New Computational Paradigms: First Conference on Computability in Europe, CiE 2005}, address = {Amsterdam, The Netherlands}, volume = {3526}, pages = {263--274}, month = {jun 8--12}, series = LNCS, publisher = Springer-Verlag, theme = {C}, site = {copenhagen} } @Article{Simonsen:Specker, AUTHOR = {Jakob Grue Simonsen}, YEAR = {2005}, TITLE = {Specker Sequences Revisited}, JOURNAL = {Mathematical Logic Quarterly}, volume = {51}, number = {5}, pages = {532--540}, theme = {I}, site = {copenhagen} } @InProceedings{Simonsen:beta, AUTHOR = {Jakob Grue Simonsen}, YEAR = {2005}, TITLE = {On Beta-Shifts Having Arithmetical Languages}, BOOKTITLE = {Proceedings of the 30th International Symposium on Mathematical Foundations of Computer Science (MFCS 2005)}, editor = {}, publisher = {Springer-Verlag}, organization = {}, address = {}, series = {Lecture Notes in Computer Science}, volume = {}, pages = {}, month = {}, theme = {I}, site = {copenhagen} } @PhDThesis{ simonsen-2005-thesis, AUTHOR = {Jakob Grue Simonsen}, YEAR = {2005}, TITLE = {On Computable Approximation of Infinite Objects}, SCHOOL = {{DIKU}, {D}ept. of {C}omputer {S}cience, {U}niversity of {C}openhagen}, address = {{U}niversitetsparken 1, DK-2100 {C}openhagen {E}ast, {D}enmark}, month = {May}, PUF = {Ph.D. afhandling}, ID = {PhD}, theme = {I}, site = {copenhagen} } @TechReport{Filinski-Rohde:UNBE-TR05, author = {Andrzej Filinski and Henning Korsholm Rohde}, title = {Denotational Aspects of Untyped Normalization by Evaluation (Extended Version, with Detailed Proofs)}, institution = {University of Aarhus, Denmark}, year = 2005, type = {BRICS Report}, number = {RS-05-4}, theme = {C}, site = {copenhagen,aarhus} } @InProceedings{KetemaSimonsen:iCRS, AUTHOR = {Ketema, Jeroen and Simonsen, Jakob Grue}, YEAR = {2005}, TITLE = {Infinitary Combinatory Reduction Systems}, BOOKTITLE = {Proceedings of the 16th International Conference on Rewriting Techniques and Applications (RTA '05)}, editor = {Giesl, J.}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {3467}, pages = {438--452}, theme = {I}, site = {copenhagen} } @Proceedings{GPCE2005, editor = {Glück, Robert and Lowry, Michael}, YEAR = {2005}, TITLE = {Generative Programming and Component Engineering}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {3676}, pages = {448}, theme = {C}, site = {copenhagen} } @InProceedings{Lawall:nwpt05, AUTHOR = {Jean-Paul Bodeveix and Mamoun Filali and Julia L. Lawall and Gilles Muller}, YEAR = {2005}, TITLE = {Applying the {B} formal method to the {Bossa} domain-specific language}, BOOKTITLE = {The 17th Nordic Workshop on Programming Theory (NWPT'05)}, organization = {}, address = {Copenhagen, Denmark}, series = {}, volume = {}, pages = {35--38}, theme = {C,D}, site = {copenhagen} } @InProceedings{Lawall:gpce05, AUTHOR = {Julia L. Lawall and Herve Duchesne and Gilles Muller and Anne-Francoise {Le Meur}}, YEAR = {2005}, TITLE = {Bossa {Nova}: Introducing modularity into the {Bossa} domain-specific language}, BOOKTITLE = {Third International Conference on Generative Programming and Component Engineering (GPCE'05)}, address = {Tallinn, Estonia}, series = {Lecture Notes in Computer Science}, volume = {3676}, pages = {78--93}, theme = {C,D}, site = {copenhagen} } @inproceedings{JJ05b, author = {Jeroen Ketema and Jakob Grue Simonsen}, YEAR = {2005}, title = {On Confluence of Infinitary Combinatory Reduction Systems}, pages = {199--214}, booktitle = {Proceedings of the 12th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2005)}, series = {Lecture notes in artificial intelligence}, volume = {3835}, publisher = {Springer-Verlag}, theme = {I}, site = {copenhagen} } @InProceedings{ ESCAR05, AUTHOR = {Klaus Grue}, YEAR = {2005}, TITLE = {The implementation of Logiweb}, BOOKTITLE = {Empirically Successful Classical Automated Reasoning (ESCAR)}, editor = {Bernd Fischer and Stepahn Schulz and Geoff Sutcliffe}, theme = {B}, site = {copenhagen} } @Article{chin:khoo:jones:05, AUTHOR={Wei-Ngan Chin, Siau-Cheng Khoo and Neil Jones.}, YEAR={2005}, TITLE={Redundant Call Elimination via Tupling}, JOURNAL={Fundamenta Informaticae}, volume={69}, number={1}, pages={1--37}, theme={C}, site = {copenhagen} } @article{HylandM:cattfe, author = {Martin Hyland and Misao Nagayama and John Power and Giuseppe Rosolini}, title = {A {C}ategory {T}heoretic {F}ormulation for {E}ngeler-style {M}odels of the {U}ntyped {$\lambda$}-{C}alculus}, pages = {\#}, year = {2006}, journal = {Electronic Notes in Theoretical Computer Science}, note = {Proceedings of MFCSIT} } @incollection{BucaloA:spaac, author = {A. Bucalo and G. Rosolini}, title = {Spaces as comonoids}, booktitle = {From {Sets and Types to Topology and Analysis: Towards Practicable Foundations for Constructive Mathematics}}, pubLisher = {Oxford University Press}, year = {2005}, editor = {L. Crosilla and P. Schuster} } @article{BucaloA:confft, author = {A. Bucalo and G. Rosolini}, title = {Completions, comonoids, and topological spaces}, JOURNAL = {Ann. Pure Appl. Logic}, FJOURNAL = {Annals of Pure and Applied Logic}, year = {2006}, volume = {137} } @InProceedings{Mogelberg:LAPLsdt:MFPS, author = {R. E. Møgelberg and L. Birkedal and G. Rosolini}, title = {Synthetic domain theory and models of linear {A}badi \& {P}lotkin logic}, year = 2005, booktitle = "Proceedings of the Twenty-first Conference on the Mathematical Foundations of Programming Semantics", pages = {\#}, year = {2005}, journal = {Electronic Notes in Theoretical Computer Science} } @InProceedings{Mogelberg:LAPL:MFPS, author = {L. Birkedal and R. E. Møgelberg and R. L. Petersen}, title = {Parametric Domain-theoretic models of polymorphic intuitionistic / linear lambda calculus}, year = 2005, booktitle = "Proceedings of the Twenty-first Conference on the Mathematical Foundations of Programming Semantics", pages = {\#}, year = {2005}, journal = {Electronic Notes in Theoretical Computer Science} } @InProceedings{Anc+Mog:FMCO-2004, author = {D. Ancona and E. Moggi}, title = {Program Generation and Components}, pdf= {http://www.disi.unige.it/person/MoggiE/ftp/fmco04.pdf}, editor = "Frank S. de Boer and Marcello M. Bonsangue and Susanne Graf", booktitle = "Formal Methods for Components and Objects: Third International Symposium, FMCO 2004, Leiden, The Netherlands, November 2--5, 2004. Revised Lectures", volume = "3167", publisher = "Springer-Verlag", year = "2005", series = LNCS, } @Article{Lagorio04b, author = "G.~Lagorio", title = "{C}apturing ghost dependencies in {J}ava sources", journal = "Journ. of Object Technology", volume = 3, number = 11, month = {December}, year = 2004, note = {Special issue: OOPS track at SAC 2004, Nicosia}, pages = {77-95}, url = {http://www.jot.fm/issues/issue_2004_12/article4} } @article{FagorziZucca05, author = {S.~Fagorzi and E.~Zucca}, title = {A Calculus for Reconfiguration}, journal = {ENTCS}, editor = {M. Fern\'andez and I. Mackie}, note = {DCM 2005 - International Workshop on Developments in Computational Models}, year = {2005}, volume = 135, number = 3, } @article{FagorziZucca05, author = {S.~Fagorzi and E.~Zucca}, title = {A Calculus for Reconfiguration}, journal = {ENTCS}, editor = {M. Fern\'andez and I. Mackie}, note = {DCM 2005 - International Workshop on Developments in Computational Models}, year = {2005}, volume = 135, number = 3, } @article{AnconaEtAl05c, author = "D.~Ancona and S.~Fagorzi and E.~Zucca", title = {A Calculus for Dynamic Reconfiguration with Low Priority Linking}, editor ={V. Bono, M. Bugliesi and S. Drossopoulou}, journal = {ENTCS}, volume = {138}, number = {2}, year = {2005}, pages = {3-35}, note = {WOOD'04 -Workshop on Object-Oriented Development}, } @InProceedings{AnconaEtAl05b, author = {D.~Ancona and G.~Lagorio and E.~Zucca}, title = {Smart Modules for {J}ava-like Languages}, booktitle={Formal Techniques for Java-like Programs 2005}, year = {2005}, month= "July", } @InProceedings{AnconaEtAl05d, author = "D.~Ancona and S.~Fagorzi and E.~Zucca", title = "Mixin Modules for Dynamic Rebinding", booktitle ="TGC 2005 - Trustworthy Global Computing, International Symposium, Revised Selected Papers", year = 2005, series = {LNCS}, publisher={Springer-Verlag}, pages = {279-298}, editor = {R. De Nicola and D. Sangiorgi}, number = {3705}, pdf = {http://www.disi.unige.it/person/FagorziS/Papers/TGC05.pdf}, } @InProceedings{AnconaEtAl05, author = "D.~Ancona and F.~Damiani and S.~Drossopoulou and E.~Zucca", title = "Polymorphic Bytecode: Compositional Compilation for {J}ava-like Languages", booktitle = {POPL05}, publisher = {ACM}, year = 2005, month= "January" } %% site = {inria}, %% theme = {A-I}, %% A. Program structuring: object-oriented programming modules %% B. Proof assistants, functional programming and dependent types %% C. Program analysis, generation and configuration %% D. Specification and verification methods %% E. Types and type inference in programming %% F. Games, sequentiality and abstact machines %% G. Semantic methods for distributed computing %% H. Resource models and web data %% I. Continuous phenomena in Computer Science %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 2005 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @string{lncs = {Lecture Notes in Computer Science}} @string{springer = {Springer-Verlag}} @string{acm = {ACM Press}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%% INRIA - subsite Rocquencourt %%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @TechReport{2005-Simonet-Pottier-HMG, site = {inria}, theme = {E}, author = "Vincent Simonet and François Pottier", title = "Constraint-Based Type Inference for Guarded Algebraic Data Types", month = jan, year = "2005", institution = "INRIA", type = "Research Report", number = "5462", abstract = "\emph{Guarded} algebraic data types subsume the concepts known in the literature as \emph{indexed types}, \emph{guarded recursive datatype constructors}, and \emph{first-class phantom types}, and are closely related to \emph{inductive types}. They have the distinguishing feature that, when typechecking a function defined by cases, every branch may be checked under different assumptions about the type variables in scope. This mechanism allows exploiting the presence of dynamic tests in the code to produce extra static type information.\par We propose an extension of the constraint-based type system {HM$(X)$} with deep pattern matching, guarded algebraic data types, and polymorphic recursion. We prove that the type system is sound and that, provided recursive function definitions carry a type annotation, type inference may be reduced to constraint solving. Then, because solving arbitrary constraints is expensive, we further restrict the form of type annotations and prove that this allows producing so-called \emph{tractable} constraints. Last, in the specific setting of equality, we explain how to solve tractable constraints.\par To the best of our knowledge, this is the first \emph{generic} and \emph{comprehensive} account of type inference in the presence of guarded algebraic data types.", URL = "http://www.inria.fr/rrrt/rr-5462.html", } @InProceedings{2005-Frisch-Hosoya-Castagna-popl, site = {inria}, theme = {H}, author = {Haruo Hosoya and Alain Frisch and Giuseppe Castagna}, title = {Parametric Polymorphism for {XML}}, booktitle = "32nd ACM symposium on Principles of Programming Languages", pages = "50-62", YEAR = {2005}, month = jan, publisher = acm, url = "http://www.cduce.org/papers/polyx.ps.gz", abstract = {Although several type systems have been investigated for XML, parametric polymorphism is rarely treated. This well-established typing discipline can also be useful in XML processing in particular for programs involving "parametric schemas," i.e., schemas parameterized over other schemas (e.g., SOAP). The difficulty in treating polymorphism for XML lies in how to extend the "semantic" approach used in the mainstream (monomorphic) XML type systems. A naive extension would be "semantic" quantification over all substitutions for type variables. However, this approach reduces to an NEXPTIME-complete problem for which no practical algorithm is known, and, moreover, the type system obtained in this way is characterized by a hardly useful expressiveness. In this paper, we propose a lighter-weight way of extending the semantic approach, where we interpret type variables as markings in data values for indicating the parameterized subparts. As a result, we can construct a sensible polymorphic type system both with a semantic flavor and a set of practical algorithms needed for typechecking. Most of these algorithms can be obtained by local modifications to existing ones for a monomorphic system.} } @InCollection{2005-Pottier-Remy-ATTAPL, site = {inria}, theme = {E}, author = "Fran{\c{c}}ois Pottier and Didier R{\'{e}}my", booktitle = "Advanced Topics in Types and Programming Languages", title = "The Essence of {ML} Type Inference", pages = "389--489", publisher = "MIT Press", year = "2005", editor = "Benjamin C. Pierce", chapter = "10", } @InProceedings{2005-Remy-icfp, site = {inria}, theme = {E}, author = "Didier Rémy", title = "Simple, partial type-inference for System {F} based on type-containment", booktitle = "Proceedings of the tenth International Conference on Functional Programming", year = "2005", month = sep, publisher = acm, url = {http://pauillac.inria.fr/~remy/publications.html#Remy/fml}, html = {http://pauillac.inria.fr/~remy/work/fml}, psgz = {http://pauillac.inria.fr/~remy/work/fml/fml-icfp.ps.gz}, pdf = {http://pauillac.inria.fr/~remy/work/fml/fml-icfp.pdf} } @INPROCEEDINGS{2005-Dicosmo-Pottier-Remy-tlca, site = {inria}, theme = {E}, AUTHOR = {Roberto {Di Cosmo} and François Pottier and Didier Rémy}, TITLE = {Subtyping Recursive Types modulo Associative Commutative Products}, psgz = {http://pauillac.inria.fr/~fpottier/publis/dicosmo-pottier-remy-tlca05.ps.gz}, pdf = {http://pauillac.inria.fr/~fpottier/publis/dicosmo-pottier-remy-tlca05.pdf}, LONG = {http://cristal.inria.fr/~fpottier/publis/dicosmo-pottier-remy-tlca05-long.ps.gz}, LONGPDF = {http://cristal.inria.fr/~fpottier/publis/dicosmo-pottier-remy-tlca05-long.pdf}, BOOKTITLE = {Seventh International Conference on Typed Lambda Calculi and Applications (TLCA'05)}, ADDRESS = {Nara, Japan}, MONTH = APR, YEAR = {2005}, series = "Lecture Notes in Computer Science", publisher = "Springer Verlag", volume = "3461", pages = "179--193", ABSTRACT = {This work sets the formal bases for building tools that help retrieve classes in object-oriented libraries. In such systems, the user provides a query, formulated as a set of class interfaces. The tool returns classes in the library that can be used to implement the user's request and automatically builds the required glue code. We propose subtyping of recursive types in the presence of associative and commutative products---that is, subtyping modulo a restricted form of type isomorphisms---as a model of the relation that exists between the user's query and the tool's answers. We show that this relation is a composition of the standard subtyping relation with equality up to associativity and commutativity of products and we present an efficient decision algorithm for it. We also provide an automatic way of constructing coercions between related types.} } @PhdThesis{2005-Bonniot-these, site = {inria}, theme = {EA}, author = {Daniel Bonniot}, title = {Typage modulaire des multi-méthodes}, school = {École des Mines de Paris}, year = 2005, month = nov } @InProceedings{2005-Frisch-Castagna-Colazzo, site = {inria}, theme = {EH}, author = {Giuseppe Castagna and Dario Colazzo and Alain Frisch}, title = {Error Mining for Regular Expression Patterns}, booktitle = "9th Italian Conference on Theoretical Computer Science", YEAR = {2005}, month = oct, pages = {160-172}, abstract = {In the design of type systems for XML programming languages based on regular expression types and patterns the focus has been over result analysis, with the main aim of statically checking that a transformation always yields data of an expected output type. While being crucial for correct program composition, result analysis is not sufficient to guarantee that patterns used in the transformation are correct. In this paper we motivate the need of static detection of incorrect patterns, and provide a formal characterization based on pattern matching operational semantics, together with locally exact type analysis techniques to statically detect them.} } @article{2005-Hirschowitz-Leroy-TOPLAS, site = {inria}, theme = {AE}, author = "Tom Hirschowitz and Xavier Leroy", title = "Mixin modules in a call-by-value setting", journal = "ACM Transactions on Programming Languages and Systems", volume = 27, number = 5, pages = "857--881", year = 2005, URL = {http://pauillac.inria.fr/~xleroy/publi/mixins-cbv-toplas.pdf}, abstract = "The ML module system provides powerful parameterization facilities, but lacks the ability to split mutually recursive definitions across modules, and does not provide enough facilities for incremental programming. A promising approach to solve these issues is Ancona and Zucca's mixin modules calculus CMS. However, the straightforward way to adapt it to ML fails, because it allows arbitrary recursive definitions to appear at any time, which ML does not support. In this paper, we enrich CMS with a refined type system that controls recursive definitions through the use of dependency graphs. We then develop a separate compilation scheme, directed by dependency graphs, that translate mixin modules down to a CBV lambda-calculus extended with a non-standard let rec construct"} @inproceedings{2005-Blazy-Leroy-ICFEM, site = {inria}, theme = {BD}, author = "Sandrine Blazy and Xavier Leroy", title = "Formal verification of a memory model for {C}-like imperative languages", booktitle = "International Conference on Formal Engineering Methods (ICFEM 2005)", year = 2005, volume = 3785, series = lncs, publisher = springer, pages = "280--299", url = "http://www.springerlink.com/openurl.asp?genre=article&id=doi:10.1007/11576280_20", abstract = " This paper presents a formal verification with the Coq proof assistant of a memory model for C-like imperative languages. This model defines the memory layout and the operations that manage the memory. The model has been specified at two levels of abstraction and implemented as part of an ongoing certification in Coq of a moderately-optimising C compiler. Many properties of the memory have been verified in the specification. They facilitate the definition of precise formal semantics of C pointers. A certified OCaml code implementing the memory model has been automatically extracted from the specifications."} @unpublished{2005-Leroy-Appel, site = {inria}, theme = {BD}, author = "Andrew W. Appel and Xavier Leroy", title = "A List-Machine Benchmark for Mechanized Metatheory", year = 2005, note = "Draft, circulated on the \texttt{poplmark} mailing list"} @unpublished{2005-Leroy-POPLmark, site = {inria}, theme = {BD}, author = "Xavier Leroy", title = "A locally nameless solution to the {POPLmark} challenge", year = 2005, month = oct, note = {available electornically}, url = "http://pauillac.inria.fr/~xleroy/POPLmark/locally-nameless/" } @Article{2005-Pottier-Skalka-Smith, site = {inria}, theme = {CE}, theme = {AG}, author = "François Pottier and Christian Skalka and Scott Smith", title = "A Systematic Approach to Static Access Control", URL = "http://cristal.inria.fr/~fpottier/publis/fpottier-skalka-smith-toplas.ps.gz", month = mar, year = "2005", volume = "27", number = "2", journal = "ACM Transactions on Programming Languages and Systems", abstract = "The Java Security Architecture includes a dynamic mechanism for enforcing access control checks, the so-called stack inspection process. While the architecture has several appealing features, access control checks are all implemented via dynamic method calls. This is a highly non-declarative form of specification which is hard to read, and which leads to additional run-time overhead. This paper develops type systems which can statically guarantee the success of these checks. Our systems allow security properties of programs to be clearly expressed within the types themselves, which thus serve as static declarations of the security policy. We develop these systems using a systematic methodology: we show that the security-passing style translation, proposed by Wallach, Appel and Felten as a dynamic implementation technique, also gives rise to static security-aware type systems, by composition with conventional type systems. To define the latter, we use the general HM(X) framework, and easily construct several constraint- and unification-based type systems." } @article{2005-Pottier-Gauthier-HOSC, site = {inria}, theme = {B}, theme = {AG}, author = "François Pottier and Nadji Gauthier", title = "Polymorphic Typed Defunctionalization and Concretization", journal = "Higher-Order and Symbolic Computation", note = "To appear", month = may, year = "2005", URL = "http://cristal.inria.fr/~fpottier/publis/fpottier-gauthier-hosc.pdf", abstract = "Defunctionalization is a program transformation that eliminates functions as first-class values. We show that defunctionalization can be viewed as a type-preserving transformation of an extension of with guarded algebraic data types into itself. We also suggest that defunctionalization is an instance of concretization, a more general technique that allows eliminating constructs other than functions. We illustrate this point by presenting two new type-preserving transformations that can be viewed as instances of concretization. One eliminates Rémy-style polymorphic records; the other eliminates the dictionary records introduced by the standard compilation scheme for Haskell's type classes." } @InProceedings{2005-Frisch-Castagna-GentleIntroduction, site = {inria}, theme = {E}, author = {Giuseppe Castagna and Alain Frisch}, title = {A Gentle Introduction to Semantic Subtyping}, booktitle = "International Conference on Principles and Practice of Declarative Programming", pages = "198-199", note = "Abstract of invited lecture", YEAR = {2005}, month = jul, publisher = acm } @Article{2005-Prevosto-Delahaye-Jaume-coqdess, site = {inria}, theme = {B}, author = {David Delahaye and Mathieu Jaume and Virgile Prevosto}, title = {Coq, un outil pour l'enseignement}, journal = {Technique et Science Informatique}, year = 2005, volume = 24, number = 9, pages = {1139-1160} } @InProceedings{2005-Pottier-AlphaCaml, site = {inria}, theme = {AE}, theme = {AG}, author = "François Pottier", title = "An overview of {C$\alpha$ml}", month = sep, year = "2005", booktitle = "ACM Workshop on ML", pages = "27--51", series = "Electronic Notes in Theoretical Computer Science", URL = "http://cristal.inria.fr/~fpottier/publis/fpottier-alphacaml.pdf", abstract = "C$\alpha$ml is a tool that turns a so-called ``binding specification'' into an Objective Caml compilation unit. A binding specification resembles an algebraic data type declaration, but also includes information about names and binding. C$\alpha$ml is meant to help writers of interpreters, compilers, or other programs-that-manipulate-programs deal with $\alpha$-conversion in a safe and concise style. This paper presents an overview of C$\alpha$ml's binding specification language and of the code that C$\alpha$ml produces." } %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 2006 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @inproceedings{2006-Pottier-Regis-Gianas-GADTs, site = {inria}, theme = {E}, theme = {AG}, author = "François Pottier and Yann Régis-Gianas", title = "Stratified type inference for generalized algebraic data types", booktitle = "33rd ACM symposium on Principles of Programming Languages", pages = "232--244", month = jan, year = "2006", publisher = acm, URL = "http://cristal.inria.fr/~fpottier/publis/pottier-regis-gianas-05.pdf", abstract = "We offer a solution to the type inference problem for an extension of Hindley and Milner's type system with generalized algebraic data types. Our approach is in two strata. The bottom stratum is a core language that marries type inference in the style of Hindley and Milner with type checking for generalized algebraic data types. This results in an extremely simple specification, where case constructs must carry an explicit type annotation and type conversions must be made explicit. The top stratum consists of (two variants of) an independent shape inference algorithm. This algorithm accepts a source term that contains some explicit type information, propagates this information in a local, predictable way, and produces a new source term that carries more explicit type information. It can be viewed as a preprocessor that helps produce some of the type annotations required by the bottom stratum. It is proven sound in the sense that it never inserts annotations that could contradict the type derivation that the programmer has in mind." } @inproceedings{2006-Leroy-Bertot-Gregoire, site = {inria}, theme = {BD}, author = "Yves Bertot and Benjamin Grégoire and Xavier Leroy", title = "A structured approach to proving compiler optimizations based on dataflow analysis", booktitle = "Types for Proofs and Programs, Workshop TYPES 2004", year = 2006, volume = 3839, pages = "66-81", series = lncs, publisher = springer, url = "http://pauillac.inria.fr/~xleroy/publi/proofs_dataflow_optimizations.pdf", abstract = " This paper reports on the correctness proof of compiler optimizations based on data-flow analysis. We formulate the optimizations and analyses as instances of a general framework for data-flow analyses and transformations, and prove that the optimizations preserve the behavior of the compiled programs. This development is a part of a larger effort of certifying an optimizing compiler by proving semantic equivalence between source and compiled code."} @inproceedings{2006-Leroy-compcert, site = {inria}, theme = {BD}, author = "Xavier Leroy", title = "Formal certification of a compiler back-end, or: programming a compiler with a proof assistant", booktitle = "33rd ACM symposium on Principles of Programming Languages", year = 2006, publisher = acm, pages = "42--54", url = "http://pauillac.inria.fr/~xleroy/publi/compiler-certif.pdf", abstract = "This paper reports on the development and formal certification (proof of semantic preservation) of a compiler from Cminor (a C-like imperative language) to PowerPC assembly code, using the Coq proof assistant both for programming the compiler and for proving its correctness. Such a certified compiler is useful in the context of formal methods applied to the certification of critical software: the certification of the compiler guarantees that the safety properties proved on the source code hold for the executable compiled code as well."} @inproceedings{2006-Leroy-coindsem, site = {inria}, theme = {BD}, author = "Xavier Leroy", title = "Coinductive big-step operational semantics", booktitle = "European Symposium on Programming (ESOP'06)", year = 2006, publisher = springer, note = "Accepted for publication, to appear", url = "http://pauillac.inria.fr/~xleroy/publi/coindsem.pdf", abstract = "This paper illustrates the use of co-inductive definitions and proofs in big-step operational semantics, enabling the latter to describe diverging evaluations in addition to terminating evaluations. We show applications to proofs of type soundness and to proofs of semantic preservation for compilers." } @InProceedings{2006-Frisch-planx, site = {inria}, theme = {H}, author = {Alain Frisch}, title = {{OCaml} + {XDuce}}, booktitle = "Programming Language Technologies for XML (PLAN-X) 2006", YEAR = {2006}, month = jan } %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%% INRIA - subsite Rennes %%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @InProceedings{Sotin:06:Quantitative, author = {Pascal Sotin and David Cachera and Thomas Jensen}, title = {Quantitative static analysis over semirings: analysing cache behaviour for Java Card}, booktitle = {Proc.~of 4th Workshop on Quantitative Aspects of Programming Languages}, year = {2006}, publisher = {Elsevier Electronic Notes in Computer Science}, site = {inria}, theme = {CH}, note = {To appear} } @INPROCEEDINGS{EAAI:BessonJensenPichardie, AUTHOR= "F. Besson and T. Jensen and D. Pichardie", TITLE= "{A PCC Architecture based on Certified Abstract Interpretation}", PUBLISHER = {Elsevier}, YEAR = 2006, SERIES = {ENTCS}, BOOKTITLE={Proc. of 1st International Workshop on Emerging Applications of Abstract Interpretation (EAAI'06)}, site = {inria}, theme = {BC} } @Article{TCSAppSem:BessonJensenPichardie, author = "F. Besson and T. Jensen and D. Pichardie", title = "Proof-Carrying Code from Certified Abstract Interpretation and Fixpoint Compression", journal = "Theoretical Computer Science", YEAR = 2006, NOTE = "To appear", site = {inria}, theme = {BC} } %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%% INRIA - subsite Rennes %%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @InProceedings{gdt06:sp, author = {G. Barthe and D. Naumann and T. Rezk}, title = {Deriving an Information Flow Checker and Certifying Compiler for Java}, booktitle = {Symposium on Security and Privacy, 2006}, pdfurl = {http://mobius.inria.fr/twiki/pub/Publications/WebHome/Barthe-Naumann-Rezk-SP06.pdf}, year = {2006}, publisher = {IEEE Press}, theme={D}, site={inria} } @INPROCEEDINGS{Gregoire-Barras-05, AUTHOR = {Bruno Barras and Benjamin Grégoire}, TITLE = {On the role of type decorations in the Calculus of Inductive Constructions}, TOPICS = {team}, URL = {http://www-sop.inria.fr/everest/personnel/Benjamin.Gregoire/Publi/equiv.ps.gz}, CROSSREF = {csl05}, theme={B}, site={inria} } @PROCEEDINGS{csl05, TITLE = {Proceedings of CSL'05}, BOOKTITLE = {Proceedings of CSL'05}, YEAR = {2005}, ADDRESS = {Oxford, UK}, MONTH = {August}, NOTE = {to appear} } @INPROCEEDINGS{BFPR06:flops, AUTHOR = {G. Barthe and J. Forest and D. Pichardie and V. Rusu}, TITLE = {{Defining and reasoning about recursive functions: a practical tool for the Coq proof assistant}}, PAGES = {114-129}, CROSSREF = {flops06}, theme={B}, site={inria}} @inproceedings{gta05:fast, author = {G. Barthe and T.Rezk and A. Saabas}, title = {{Proof obligations preserving compilation}}, year = {2005}, booktitle="Proceedings of FAST'05", OPTeditor="R.~Gorrieri and F.~Martinelli and P.~Ryan and S.~Schneider", series=lncs, volume={3xxx}, publisher=springer, note="To appear", theme={D}, site={inria}} @PROCEEDINGS{flops06, BOOKTITLE = {Proceedings of FLOPS'06}, TITLE = {Proceedings of FLOPS'06}, YEAR = 2006, PUBLISHER = {Springer-Verlag}, SERIES = {Lecture Notes in Computer Science}, VOLUME = 3945, EDITOR = {Masimi Hagiya and Philip Wadler} } @PROCEEDINGS{sp06, BOOKTITLE = {Proceedings of Symposium of Security and Privacy '06}, TITLE = {Proceedings of Proceedings of Symposium of Security and Privacy '06}, YEAR = 2006, PUBLISHER = {IEEE Press ()}, SERIES = {}, EDITOR = {}, NOTE = {to appear} } %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @INPROCEEDINGS{gnaedig05b, AUTHOR = {Gnaedig, Isabelle and Kirchner, Hélène}, TITLE = {Termination of rewriting strategies,: a generic approach}, BOOKTITLE = {{Proceedings of the APPSEM II Workshop 2005, Chiemsee, Germany}}, YEAR = {2005}, EDITOR = {Martin Hofmann and Hans-Wolfgang Loidl}, MONTH = {Sep}, PUBLISHER = {APPSEM II \& Ludwig Maximilians Universit\"at M\"unchen}, KEYWORDS = {rewriting, termination, strategy, innermost, outermost, local strategy, induction, narrowing, abstraction, ordering constraint}, ABSTRACT = {We propose a generic termination proof method for rewriting under strategies, based on an explicit induction on the termination property. Rewriting trees on ground terms are modelized by proof trees, generated by alternatively applying narrowing and abstracting steps. The induction principle is applied through the abstraction mechanism, where terms are replaced by variables representing any of their normal forms. The induction ordering is not given a priori, but defined with ordering constraints, incrementally set during the proof. The generic method is then instantiated for the innermost strategy, as an example.} } @InProceedings{BKMappsem05, author = {Guillaume Bonfante, Matthieu Kaczmarek and Jean-Yves Marion}, title = {Abstract Detection of Computer Viruses}, booktitle = {{Proceedings of the APPSEM II Workshop 2005, Chiemsee, Germany}}, year = 2005, editor = {Martin Hofmann and Hans-Wolfgang Loidl} } @InProceedings{FGMMNappsem05, author = {Pascal Fontaine, Kamal Gupta, Jean-Yves Marion, Stephan Merz, et Leonor Nieto}, title = {Towards a Combination of Heterogeneous Deductive Tools for System Verification: A Case Study on Clock Synchronization}, booktitle = {{Proceedings of the APPSEM II Workshop 2005, Chiemsee, Germany}}, year = 2005, editor = {Martin Hofmann and Hans-Wolfgang Loidl} } @InProceedings{MMappsem05, author = {Jean-Yves Marion et Jean-Yves Moyen}, title = {Termination and Non Size Increasingness of assembly programs}, booktitle = {{Proceedings of the APPSEM II Workshop 2005, Chiemsee, Germany}}, year = 2005, editor = {Martin Hofmann and Hans-Wolfgang Loidl} } %%%%%%%%%%%%%%%% @INPROCEEDINGS{MP06, AUTHOR = {J-Y Marion and R. P\'echoux}, TITLE = {Resource Analysis by Sup-interpretation}, BOOKTITLE = {FLOPS}, YEAR = 2006, VOLUME = 3945, SERIES = {Lecture Notes in Computer Science}, PAGES = {163--176}, PUBLISHER = {Springer}, URL = {Articles/flops06.pdf} } @ARTICLE{BCdNM06, AUTHOR = {O. Bournez and F. Cucker and P.J. de Naurois and J.Y. Marion}, TITLE = {Implicit complexity over an arbitrary structure: Quantifier alternations}, JOURNAL = {Information and Computation}, YEAR = 2006, VOLUME = 204, NUMBER = 2, PAGES = {210-230}, MONTH = {Feb}, URL = {Articles/ic06.pdf} } @INPROCEEDINGS{BMM05a, AUTHOR = {Guillaume Bonfante and Jean-Yves Marion and Jean-Yves Moyen}, TITLE = {Quasi-interpretations and Small Space Bounds.}, BOOKTITLE = {Term Rewriting and Applications, 16th International Conference, RTA 2005, Nara, Japan, April 19-21, 2005, Proceedings}, EDITOR = {Jürgen Giesl}, YEAR = {2005}, PAGES = {150-164}, PUBLISHER = {Springer}, SERIES = {Lecture Notes in Computer Science}, VOLUME = {3467}, URL = {Articles/rta05.pdf} } @ARTICLE{BCdNM05, AUTHOR = {Olivier Bournez and Felipe Cucker and Paulin Jacobé de Naurois and Jean-Yves Marion}, TITLE = {Implicit Complexity over an Arbitrary Structure: Sequential and Parallel Polynomial Time.}, JOURNAL = {Journal of Logic and Computation}, VOLUME = {15}, NUMBER = {1}, YEAR = {2005}, PAGES = {41-58}, URL = {Articles/jlc05.pdf} } %%%%%%%%% Thema D %%%%%%%%%%% @INPROCEEDINGS{MFMNT06, AUTHOR = {Pascal Fontaine and Jean-Yves Marion and Stephan Merz and Leonor Prensa Nieto and Alwen Tiu}, TITLE = {Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants}, BOOKTITLE = {TACAS}, YEAR = 2006, SERIES = {Lecture Notes in Computer Science}, PAGES = {167--181}, VOLUME = {3920}, PUBLSIHER = {Springer}, URL = {Articles/tacas06.pdf} } @ARTICLE{Gal05a, AUTHOR = {D. Galmiche and D. M\'ery and D.Pym}, TITLE = {The Semantics of {BI} and {R}esource {T}ableaux}, JOURNAL = MSCS, YEAR = {2005}, VOLUME = {15}, NUMBER ={6}, PAGES = {1033-1088}, NOTE = {} } @ARTICLE{Gal05b, AUTHOR = {D. Galmiche and D. M\'ery}, TITLE = {Resource Graphs and Countermodels in Resource Logics}, JOURNAL = ENTCS, YEAR = {2005}, VOLUME = {125}, NUMBER ={3}, PAGES = {117-135}, NOTE = {} } @CONFERENCE{Gal05c, AUTHOR = {D. Galmiche and D. M\'ery}, TITLE = {Characterizing Provability in {BI}'s Pointer Logic through Resource Graphs}, BOOKTITLE = {Int. Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2005, LNAI 3835}, YEAR = {2005}, PAGES = {459-473}, ADDRESS = {Montego Bay, Jamaica}, MONTH = {December}, NOTE = {} } @CONFERENCE{Gal05d, AUTHOR = {E. Dumoulin and D. Galmiche}, TITLE = {Labelled Structures and Provability in Resource Logics - extended abstract}, BOOKTITLE = {Int. Workshop on Structures and Deduction, SD'05}, YEAR = {2005}, PAGES = {}, ADDRESS = {Lisbon, Portugal}, MONTH = {July}, NOTE = {Satellite Workshop of ICALP 2005} } @CONFERENCE{Gal05e, AUTHOR = {N. Biri and D. Galmiche}, TITLE = {Resource Trees and XML Data Transformations - abstract}, BOOKTITLE = {3rd Applied Semantics Workshop, APPSEM05}, YEAR = {2005}, PAGES = {}, ADDRESS = {Frauenchiemsee, Germany}, MONTH = {September}, NOTE = {} } @INPROCEEDINGS{DRC-APPSEM2005, AUTHOR = {Cansell, D. and Méry, D.}, TITLE = {Formal and Incremental Construction of a Distributed Reference Counting Algorithm}, BOOKTITLE = {{APPSEM 2005}}, YEAR = 2005, EDITOR = {Hoffmann, M. and Loidl, H.-W.}, MONTH = sep } @ARTICLE{mery05a, CRINNUMBER = {A05-R-030}, CATEGORY = {1}, EQUIPE = {MOSEL}, AUTHOR = {Méry, D. and Cansell, D. and Proch, C. and Abraham, D. and Ditsch, P.}, TITLE = {The challenge of {QoS} for digital television services}, JOURNAL = {EBU Technical Review}, YEAR ={2005}, MONTH = apr, KEYWORDS = {model, refinement, proof, dvb-t}, } @INPROCEEDINGS{abrial05a, CRINNUMBER = {A05-R-031}, CATEGORY = {3}, AUTHOR = {Abrial, J.-R. and Cansell, D. and Méry, D.}, TITLE = {Refinement and Reachability in Event\_B}, BOOKTITLE = {{ZB 2005: Formal Specification and Development in Z and B}}, address = {Guilford, UK}, YEAR ={2005}, EDITOR = {H. Treharne and S. King and M. Henson}, VOLUME = {3455}, SERIES = {Lecture Notes in Computer Science}, PAGES = {222--241}, MONTH = apr, PUBLISHER = {Springer Verlag}, KEYWORDS = {refinement, stuttering, reachability, b method}, } @article{ABRIAL:2005:31564, title={Formal Construction of a Non-blocking Concurrent Queue Algorithm (a Case Study in Atomicity)}, author={Abrial, J.-R. and Cansell, D.}, booktitle={Atomicity in System Design and Execution (Proceedings of Dagstuhl-Seminar 04181)}, publisher={Springer}, pages={744--770}, journal={Journal of Universal Computer Science}, volume={11}, number={5}, year = 2005, URL={http://hal.inria.fr/inria-00000120/en/}, } %% inria-00000196, version 1 %% http://hal.inria.fr/inria-00000196/en/ @article{CANSELL:2005:35645, title={Un syst\`{e}me d'analyse de la qualit\'{e}: de la norme au produit en passant par le raffinement}, author={Cansell, D. and M\'{e}ry, D. and Proch, C.}, publisher={CNAM - Paris, France}, pages={44--50}, journal={G\'{e}nie logiciel}, number={73}, year = 2005, URL={http://hal.inria.fr/inria-00000196/en/}, } @inproceedings{ABRAHAM:2005:42053, title={Synthesis of the {QoS} for digital {TV} services}, author={Abraham, D. and Cansell, D. and Ditsch, P. and M\'{e}ry, D. and Proch, C.}, booktitle={First International Workshop on Incentive Based Computing - IBC'05}, address={Amsterdam, The Netherlands}, year = 2005, URL={http://hal.inria.fr/inria-00000565/en/}, } %% inria-00000564, version 1 %% http://hal.inria.fr/inria-00000564/en/ @inproceedings{CANSELL:2005:42051, title={Modelling SystemC scheduler by refinement}, author={Cansell, D. and M\'{e}ry, D. and Proch, C.}, booktitle={IEEE ISoLA Workshop on Leveraging Applications of Formal Methods, Verification, and Validation - ISOLA'05}, address={Columbia, U.S.A.}, year = 2005, URL={http://hal.inria.fr/inria-00000564/en/}, } % ---- 2005 -------------------------------------------------------------------- % ---- Journal Papers + Book chapters @article{CP05, author = "Cunha, A. and Pinto, J. S.", title = "Point-free Program Transformation", journal = "Fundamenta Informaticae (Special issue on Program Transformation)", volume = "66", number = "4", pages = "315--352", publisher = "IOS Press", year = "2005" } @article{BCP05, author = "Barbosa, M. and Cunha, A. and Pinto, J. S.", title = "Recursion Patterns and Time-analysis", journal = "{ACM SIGPLAN Notices}", volume = "40", number = "5", pages = "45--54", publisher = "ACM Press", year = "2005" } @Article{CBO05, author = "A. Cruz and L. Barbosa and J. Oliveira", title = "From Algebras to Objects: Generation and Composition", journal = "Journal of Universal Computer Science", year = "2005", volume = "11", number = "10", pages = "1580--1612", } % ---- Conference Papers @inproceedings{CPP05, author = "Cunha, A. and Pinto, J. S. and Proen\c{c}a, J.", title = "A Framework for Point-free Program Transformation", booktitle = "Selected Papers from 17th Workshop on Implementation and Application of Functional Preogramming", publisher = "Springer Lect. Notes Comp. Sci. (to appear)", year = "2005" } @inproceedings{SC06, author = "João Costa Seco and Lu\'{\i}s Caires", title = "Types for Dynamic Reconfiguration", booktitle = "In Proceedings of the European Symposium on Programming (ESOP)", publisher = "Springer-Verlag, LNCS", pages = "214-229", year = "2006" } @inproceedings{SC05, author = "João Costa Seco and Lu\'{\i}s Caires", title = "Subtyping First-Class Polymorphic Components", booktitle = "In Proceedings of the European Symposium on Programming (ESOP)", publisher = "Springer-Verlag, LNCS", pages = "342-356", year = "2005" } @inproceedings{ASVO05, author = "Alves, T. and Silva, P. and Visser, J. and Oliveira, J. N.", title = "Strategic Term Rewriting and its Application to a {VDM-SL} to {SQL} Conversion", booktitle = "13th Int. Symp. on Formal Methods ({FM 2005})", editor = "Fitzgerald, J. and Hayes, I. J. and Tarlecki, A.", address = "Newcastle upon Tyne, UK", month = "July", publisher = "Springer Lect. Notes Comp. Sci. (3582)", pages = "399--414", year = "2005" } @inproceedings{SCS06, author = "José Carlos Silva, José Campos and João Saraiva", title = "Combining Formal Methods and Functional Strategies Regarding the Reverse Engineering of Interactive Applications", booktitle = "XIII International Workshop on Design, Specification and Verification of Interactive Systems", publisher = "Springer Lect. Notes Comp. Sci. (to appear)", year = "2006" } @inproceedings{MBZ05, author = "Sun, M. and Barbosa, L. S. and Naixiao, Z.", title = "On Refinement of Software Architectures", booktitle = "2nd Int. Colloquium on Theorectical Aspects of Computing ({ICTAC'05})", editor = "Dang Van Hung and Martin Wirsing", address = "Hanoi, Vietnam", month = "October", publisher = "Springer Lect. Notes Comp. Sci. (3722)", pages = "469--484", year = "2005" } @inproceedings{SABZ05, author = "Sun, M. and Aichernig, B. K. and Barbosa, L. S. and Naixiao, Z.", title = "A Coalgebraic Semantic Framework for Component Based Development in {UML}", booktitle = "Proc. Int. Conf. on Category Theory and Computer Science (CTCS'04)", editor = "Birkedal, L.", publisher = {Elect. Notes in Theor. Comp. Sci., Elsevier}, volume = "122", pages = "229--245", year = "2005" } @article{RB05, author = "Rodrigues, Nuno F. and Barbosa, L. S.", title = {Architectural Prototyping: From CCS to .Net.}, journal = "Electr. Notes Theor. Comput. Sci.", volume = "130", year = 2005, pages = "151--167" } @inproceedings{marcoESEC05, author = "Barbosa, M.", title = "A Refinement Calculus for Software Components and Architectures", booktitle = "Proc. Doctoral Symposium at ESEC/FSE'05 (Joint Meeting of the 10th European Software Engineering Conf. and the 13th ACM SIGSOFT Int. Symp. on Foundations of Software Engineering)", month = "September", address = "New University of Lisbon", year = "2005" } % ---- In Preparation @article{ JP, author = " J. Esp\'{\i}rito Santo and L.Pinto ", title = "A calculus of multiary sequent terms ", note = "In preparation", } % ------- Talks @inproceedings{Cairesa, author = "Lu\'{\i}s Caires", title = "Composing Distributed Services with Spatial Types", booktitle = "Keynote talk at FMCO'05", year = "2005" } @inproceedings{Cairesb, author = "Lu\'{\i}s Caires", title = "Proof techniques for Distributed Processes and Resources based on Spatial Logic", booktitle = "Invited Talk at TGC'05, ETAPS'05", year = "2005" } @inproceedings{JES05, author = "J. Esp\'{\i}rito Santo", title = "Unity in structural proof theory and structural extensions of the lambda-calculus", booktitle = "talk at 4th Workshop on Proof, Computation and Complexity", year = "2005" } @inproceedings{JFP05, author = "J. Esp\'{\i}rito Santo, M.J. and L. Pinto", title = "Redundancies in an extension of the lambda-calculus and natural fragments of sequent calculus", bootitle = "talk at 4th Workshop on Proof, Computation and Complexity", year = "2005" } % ---- Thesis % ----- Technical Report @techreport{PintoJS:funpptintr, author = "I.~Mackie, J.~S. Pinto, and M.~Vila\c{c}a", title = "Functional programming and program transformation with interaction nets", type = {Technical Report DI-PURe-05.05.02}, institution = { Departamento de Inform\'atica, Universidade do Minho}, month = {October}, year = 2004 } @techreport{VCV05, author = "H. Vieira, L. Caires and R. Viegas", title = "The Spatial Logic Model Checker User's Manual and Tutorial" , type = {Technical Report DI/FCT/UNL 5/2005}, institution = { Departamento de Inform\'atica, Universidade Nova de Lisboa}, year = "2005" } @inproceedings{DBLP:conf/fsttcs/LagoH05, author = {Ugo Dal Lago and Martin Hofmann}, title = {Quantitative Models and Implicit Complexity.}, booktitle = {FSTTCS, Springer LNCS3821}, year = {2005}, pages = {189-200}, editors = {R Ramanujam and Sandeep Sen} } @inproceedings{DBLP:conf/lics/Hofmann05, author = {Martin Hofmann}, title = {Proof-Theoretic Approach to Description-Logic.}, title = {20th IEEE Symposium on Logic in Computer Science (LICS 2005), 26-29 June 2005, Chicago, IL, USA, Proceedings}, year = {2005}, pages = {229-237}, ee = {http://dx.doi.org/10.1109/LICS.2005.38}, crossref = {DBLP:conf/lics/2005}, bibsource = {DBLP, http://dblp.uni-trier.de} } @proceedings{DBLP:conf/lics/2005, title = {20th IEEE Symposium on Logic in Computer Science (LICS 2005), 26-29 June 2005, Chicago, IL, USA, Proceedings}, booktitle = {LICS}, publisher = {IEEE Computer Society}, year = {2005}, isbn = {0-7695-2266-1}, bibsource = {DBLP, http://dblp.uni-trier.de} } @InProceedings{Nilsson2005a, theme = {BE}, author = "Henrik Nilsson", title = "Dynamic Optimization for Functional Reactive Programming using Generalized Algebraic Data Types", booktitle = "Proceedings of the Tenth {ACM} {SIGPLAN} International Conference on Functional Programming (ICFP'05)", pages = "54--65", year = 2005, address = "Tallinn, Estonia", month = sep, publisher = "{ACM} Press" } @inproceedings{ghani-rta05, theme = {D}, author = {Neil Ghani, Christoph Luth, Michael Abbott}, title = {Abstract modularity}, booktitle = {Proceedings of RTA 2005}, volume = {LNCS}, issue = {3467}, pages = {46-60}, publisher = {Springer Verlag}, year = {2005} } @inproceedings{ghani-icfp05, theme = {B}, author = {Neil Ghani and Patricia Johann and Tarmo Uustalu and Varmo Vene}, title = {Monadic augment and generalised short cut fusion.}, booktitle = {ICFP}, year = {2005}, pages = {294-305} } @article{ghani-mscs05, theme = {D}, author = {Neil Ghani and Christoph Lüth and Federico De Marchi}, title = {Monads of coalgebras: rational terms and term graphs.}, journal = {Mathematical Structures in Computer Science}, volume = {15}, number = {3}, year = {2005}, pages = {433-451} } @TechReport{CROrarh, theme = {D}, author = {Roy L. Crole}, title = {{A Representational Adequacy Result for Hybrid}}, institution = {University of Leicester, Department of Computer Science}, month = {April}, year = {2005}, } @article{kr:mscs05, theme = {D}, optauthor = {A. Kurz and J. Rosický}, author = {Alexander Kurz and Ji{\v r}{\'\i} Rosický}, title = {Operations and Equations for Coalgebras}, year = {2005}, journal = {Math.\ Structures Comput.\ Sci.}, optpages = {149--166}, volume = {15}, } @InProceedings{bk:fossacs05, theme = {D}, author = {Marcello Bonsangue and Alexander Kurz}, booktitle = {FoSSaCS'05}, title = {Duality for Logics of Transition Systems}, year = {2005}, series = {LNCS}, volume = {3441}, editor = {V. Sassone}, OPTannote = {} } @Article{kp:mscs05, theme = {D}, optauthor = {A. Kurz and D. Pattinson}, author = {Alexander Kurz and Dirk Pattinson}, title = {Coalgebraic Modal Logic of Finite Rank}, journal = {Math.\ Structures Comput.\ Sci.}, year = {2005}, volume = {15}, pages = {453--473}, } @inproceedings{kkp:calco05, theme = {D}, author = {Clemens Kupke and Alexander Kurz and Dirk Pattinson}, title = {Ultrafilter Extensions of Coalgebras}, OPTeditor = {J. Fiadeiro and N. Harmann and M. Roggenbach and J. Rutten}, optbooktitle = "Algebra and Coalgebra in Computer Science", booktitle = {CALCO 2005}, series = {LNCS 3629}, optvolume = {}, year = {2005}, } @Article{kr:weak, theme = {G}, author = {A. Kurz and J. Rosický}, title = {Weak Factorizations, Fractions and Homotopies}, journal = {Applied Categorical Structures}, year = {2005}, volume = {13}, pages = {141-160}, } @inproceedings{a, theme = {B}, author="L. A. Dennis and P. Nogueira", editor="J. Hurd and E. Smith and A. Darbari", pages="45--58", title="What can be Learned from Failed Proofs of Non-Theorems?", booktitle="Theorem Proving in Higher Order Logics (TPHOLs 2005): Emerging Trends Proceedings", note="Technical Report PRG-RP-05-2, Oxford University Computer Laboratory", year=2005} @inproceedings{b, theme= {B}, author="L. A. Dennis and R. Monroy and P. Nogueira", editor="H. Nilsson", pages="131--141", title="Proof-directed Debugging and Repair", booktitle="Seventh Symposium on Trends in Functional Programming (TFP 2006)", year=2006} %% This message has been checked for viruses but the contents of an attachment %% may still contain software viruses, which could damage your computer system: %% you are advised to perform your own checks. Email communications with the %% University of Nottingham may be monitored as permitted by UK legislation. @STRING{PROC = "Proc. of "} @STRING{LNCS = "LNCS"} @STRING{DATAX = "Workshop on Database Technologies for Handling XML Information on the Web (DataX)"} @STRING{PLANX = "Workshop on Programming Language Technologies for XML (PLAN-X)"} @STRING{DBPL = "Data Base Programming Languages (DBPL)"} @string{IC = "Information and Computation"} @string{JFP = "Journal of Functional Programming (JFP)"} @ARTICLE{CarGheGor05-ic, author="L. Cardelli and G. Ghelli and A. D. Gordon", title="Secrecy and Group Creation", journal = IC, volume = {196}, number = {2}, year = {2005}, pages = {127--155}, theme = {E,G}, site = {pisa,microsoft} } @UNPUBLISHED{DawGarGhe-complexity, author="A. Dawar and P. Gardner and G. Ghelli", title="Expressiveness and Complexity of Graph Logic", note="In preparation", theme = {H}, site = {pisa,imperial} } @INPROCEEDINGS{GheReSim06-datax, author = "Giorgio Ghelli and Christopher R\'e and J\'er\^ome Sim\'eon", title = "{XQuery!}: An {XML} Query Language With Side Effects", booktitle = PROC # DATAX, series = LNCS, year = 2006, note = "To appear", theme = {H}, site = {pisa} } @INPROCEEDINGS{CS05-planx, author = {D. Colazzo and C. Sartiani}, title = {Typechecking Queries for Maintaining Schema Mappings in {XML} {P2P} Databases}, booktitle = PROC # PLANX, year = 2005, theme = {E,H}, site = {pisa} } @INPROCEEDINGS{CS05-dbpl, author = {D. Colazzo and C. Sartiani}, title = {Mapping Maintenance in {XML} {P2P} Databases}, booktitle = PROC # DBPL, year = 2005, series = LNCS, number = 3774, pages = {74--89}, theme = {E,H}, site = {pisa} } @ARTICLE{ColGheAl06-jfp, author = "D. Colazzo and G. Ghelli and P. Manghi and C. Sartiani", title = "Static Analysis for Path Correctness of {XML} Queries", journal = jfp, year = 2006, note = "To appear", theme = {E,H}, site = {pisa} } @ARTICLE{ColGhe05-ic, author = "D. Colazzo and G. Ghelli", title = "Subtyping, Recursion and Parametric polymorphism in {K}ernel {F}un", journal = IC, volume = 198, number = 2, year = 2005, pages = {71--147}, theme = {E}, site = {pisa} } %% 2006 ???????????????????????????????????????????????????? @Article{MRGTCS, author = {David Aspinall and Lennart Beringer and Martin Hofmann and Hans-Wolfgang Loidl and Alberto Momigliano}, title = {{A Program Logic for Resources}}, journal = {{Theoretical Computer Science}}, year = 2006, note = {To appear} } @InProceedings{StrongMobility, author = {Andre Rauber {Du Bois} and Phil Trinder and Hans-Wolfgang Loidl}, title = {{Strong Mobility using a Continuation Monad}}, booktitle = {{SBLP'06: 10th Brazilian Symposium on Programming Languages}}, year = 2006, address = {Itatiaia, Brazil, May 15-17}, note = {Accepted} } %% 2005 from here on @InProceedings{MRGsummary, author = {Donald Sannella and Martin Hofmann and David Aspinall and Stephen Gilmore and Ian Stark and Lennart Beringer and Hans-Wolfgang Loidl and Kenneth MacKenzie and Alberto Momigliano and Olha Shkaravska}, title = {{Mobile Resource Guarantees}}, year = 2005, booktitle = {Trends in Functional Programing}, address = {Tallinn, Estonia, Sep 23--24}, volume = 6, publisher = {Intellect}, pdf = {mrg-sum.pdf} } @InProceedings{Mdorf, author = {Martin Hofmann and Hans-Wolfgang Loidl and Lennart Beringer}, title = {{Certification of Quantitative Properties of Programs}}, booktitle = {{Logical Aspects of Secure Computer Systems}}, year = 2005, address = {Marktoberdorf, Aug 2-13}, publisher = {IOS Press}, note = {Lecture Notes of the Marktoberdorf Summer School 2005. To appear}, pdf = {mdorf.pdf} } @Article{mHaskell, author = {Andre Rauber {Du Bois} and Phil Trinder and Hans-Wolfgang Loidl}, title = {{mHaskell: Mobile Computation in a Purely Functional Language}}, journal = {{Journal of Universal Computer Science}}, year = 2005, volume = 11, number = 7, pages = {1234--1254}, note = {Selected papers from the SBLP'05: 9th Brazilian Symposium on Programming Languages, Recife, Brazil, May 23-25, 2005} } @InProceedings{GridGUM, author = {Abyd {Al Zain} and Phil Trinder and Hans-Wolfgang Loidl and Greg Michaelson}, title = {{Managing Heterogeneity in a Grid Parallel Haskell}}, booktitle = {{PAPP'05: Second International Workshop on Practical Aspects of High-level Parallel Programming}}, year = 2005, address = {Atlanta, GA, May 22--25} } %% Workshop 2004, Journal special issue 2005 @Article{MobilitySkeletons, author = {Andre Rauber {Du Bois} and Phil Trinder and Hans-Wolfgang Loidl}, title = {{Towards Mobility Skeletons}}, journal = {{Parallel Processing Letters}}, year = 2005, volume = 15, number = 3, pages = {273--288}, note = {Selected papers of CMPP'04 --- Intl. Workshop on Constructive Methods for Parallel Programming, Stirling, Scotland, UK, July 2004} } @Article{Ager-al:IPL04, author = {Mads Sig Ager and Olivier Danvy and Jan Midtgaard}, title = {A Functional Correspondence between Call-by-Need Evaluators and Lazy Abstract Machines}, journal = {Information Processing Letters}, year = {2004}, volume = {90}, number = {5}, pages = {223-232}, note = {Extended version available as the technical report BRICS-RS-04-3} } @Article{Ager-al:TCS??, author = {Mads Sig Ager and Olivier Danvy and Jan Midtgaard}, title = {A Functional Correspondence between Monadic Evaluators and Abstract Machines for Languages with Computational Effects}, journal = {Theoretical Computer Science}, year = {2005}, note = {Accepted for publication. Extended version available as the technical report BRICS RS-04-28} } @Article{Ager-al:TOPLAS??, author = {Mads Sig Ager and Olivier Danvy and Henning Korsholm Rohde}, title = {Fast Partial Evaluation of Pattern Matching in Strings}, journal = {ACM Transactions on Programming Languages and Systems}, year = {2005}, note = {Accepted for publication} } @TechReport{Ager:RS-04-20, author = {Mads Sig Ager}, title = {From Natural Semantics to Abstract Machines}, year = {2004}, month = {October}, number = {BRICS RS-04-20}, type = {Technical Report}, institution = {DAIMI, Department of Computer Science, University of Aarhus}, address = {Aarhus, Denmark}, note = {To appear in the proceedings of the 2004 International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR 2004)} } @InProceedings{Biernacka-al:CW04, key = {Thielecke}, author = {Ma{\l}gorzata Biernacka and Dariusz Biernacki and Olivier Danvy}, title = {An Operational Foundation for Delimited Continuations}, booktitle = {Proceedings of the Fourth ACM SIGPLAN Workshop on Continuations}, editor = {Hayo Thielecke}, year = {2004}, month = {January}, series = {Technical report CSR-04-1, Department of Computer Science, Queen Mary's College}, pages = {25-33}, address = {Venice, Italy} } @InProceedings{Biernacki-Danvy:LOPSTR03, key = {Bruynooghe}, author = {Dariusz Biernacki and Olivier Danvy}, title = {From Interpreter to Logic Engine by Defunctionalization}, booktitle = {Logic Based Program Synthesis and Transformation, 13th International Symposium, LOPSTR 2003}, editor = {Maurice Bruynooghe}, year = {2003}, month = {August}, series = {Lecture Notes in Computer Science}, number = {3018}, pages = {143-159}, publisher = {Springer-Verlag}, address = {Uppsala, Sweden} } @Article{Danvy-Schultz:JFLP04, author = {Olivier Danvy and Ulrik P. Schultz}, title = {Lambda-Lifting in Quadratic Time}, journal = {Journal of Functional and Logic Programming}, year = {2004}, month = {July}, volume = {10}, number = {1}, note = {Available online at \url{http://danae.uni-muenster.de/lehre/kuchen/JFLP/}} } @InProceedings{Danvy:CW04, key = {Thielecke}, author = {Olivier Danvy}, title = {On Evaluation Contexts, Continuations, and the Rest of the Computation}, booktitle = {Proceedings of the Fourth ACM SIGPLAN Workshop on Continuations}, editor = {Hayo Thielecke}, year = {2004}, month = {January}, series = {Technical report CSR-04-1, Department of Computer Science, Queen Mary's College}, pages = {13-23}, address = {Venice, Italy}, note = {Invited talk} } @InProceedings{Danvy:IFL04, key = {Grelck and Huch}, author = {Olivier Danvy}, title = {A Rational Deconstruction of {L}andin's {SECD} Machine}, booktitle = {Implementation and Application of Functional Languages, 16th International Workshop, IFL'04}, editor = {Clemens Grelck and Frank Huch}, year = {2004}, month = {September}, series = {Technical Report 0408}, pages = {317-334}, publisher = {Christian-Albrechts-Universität zu Kiel, Institut für Informatik und Praktische Mathematik}, address = {Lübeck, Germany} } @InProceedings{Danvy:WRS04, key = {Antoy and Toyama}, author = {Olivier Danvy}, title = {Normalization by Evaluation}, booktitle = {Proceedings of the Fourth International Workshop on Reduction Strategies in Rewriting and Programming (WRS'04)}, editor = {Sergio Antoy and Yoshihito Toyama}, year = {2004}, month = {May}, series = {Electronic Notes in Theoretical Computer Science}, address = {Aachen, Germany}, note = {Invited talk} } %Theme A. Program structuring: object-oriented programming modules @InProceedings{SHBSN05, author = {Gareth Stoyle and Michael Hicks and Gavin Bierman and Peter Sewell and Iulian Neamtiu}, title = {\textit{Mutatis Mutandis}: Safe and Predictable Dynamic Software Updating}, OPTcrossref = {}, OPTkey = {}, booktitle = {Proceedings of POPL 2005: The 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Long Beach)}, OPTpages = {}, year = {2005}, OPTeditor = {}, OPTvolume = {}, OPTnumber = {}, OPTseries = {}, OPTaddress = {}, month = jan, OPTorganization = {}, OPTpublisher = {}, OPTnote = {To appear}, OPTannote = {} } % Theme A. Program structuring: object-oriented programming modules @InProceedings{LNSW04, author = {James Leifer and Michael Norrish and Peter Sewell and Keith Wansbrough}, title = {Acute and {TCP}: specifying and developing abstractions for global computation}, OPTcrossref = {}, OPTkey = {}, booktitle = {Proceedings of the APPSEM II Workshop, Tallinn. 2pp}, pages = {}, year = {2004}, OPTeditor = {}, OPTvolume = {}, OPTnumber = {}, OPTseries = {}, OPTaddress = {}, month = apr, OPTorganization = {}, OPTpublisher = {}, OPTnote = {}, OPTannote = {} } %Theme ? @Misc{SW04, OPTkey = {}, author = {Peter Sewell and Keith Wansbrough}, title = {Applied Semantics: Specifying and Developing Abstractions for Distributed Computation (Grand Challenge Discussion Paper -- {GC2}, {GC4}, and {GC6})}, howpublished = {Position paper for Grand Challenge meeting, Newcastle. 5pp}, OPTmonth = {}, year = {2004}, OPTnote = {}, OPTannote = {} } %Theme H. Resource models and web data @InProceedings{BS04a, author = {Moritz Y. Becker and Peter Sewell}, title = {Cassandra: Distributed Access Control Policies with Tunable Expressiveness}, OPTcrossref = {}, OPTkey = {}, booktitle = {Proceedings of POLICY 2004: IEEE 5th International Workshop on Policies for Distributed Systems and Networks}, OPTpages = {}, year = {2004}, OPTeditor = {}, OPTvolume = {}, OPTnumber = {}, OPTseries = {}, OPTaddress = {}, month = jun, OPTorganization = {}, OPTpublisher = {}, note = {}, OPTannote = {} } %Theme H. Resource models and web data @InProceedings{BS04b, author = {Moritz Y. Becker and Peter Sewell}, title = {Cassandra: Flexible Trust Management, Applied to Electronic Health Records}, OPTcrossref = {}, OPTkey = {}, booktitle = {Proceedings of CSFW 2004: 17th IEEE Computer Security Foundations Workshop}, OPTpages = {}, year = {2004}, OPTeditor = {}, OPTvolume = {}, OPTnumber = {}, OPTseries = {}, OPTaddress = {}, month = jun, OPTorganization = {}, OPTpublisher = {}, note = {}, OPTannote = {} } %Theme A. Program structuring: object-oriented programming modules @TechReport{BHSSW04-tr, author = {Gavin Bierman and Michael Hicks and Peter Sewell and Gareth Stoyle and Keith Wansbrough}, title = {Dynamic Rebinding for Marshalling and Update, with Destruct-time $\lambda$}, institution = {University of Cambridge Computer Laboratory}, year = {2004}, OPTkey = {}, OPTtype = {}, number = {UCAM-CL-TR-568}, OPTaddress = {}, month = feb, OPTnote = {}, OPTannote = {} } %Theme G. Semantic methods for distributed computing @InProceedings{FS04, author = {M. P. Fiore and S. Staton}, title = {Comparing operational models of name-passing process calculi}, OPTcrossref = {}, OPTkey = {}, booktitle = { In 7th International Workshop on Coalgebraic Methods in Computer Science (CMCS'04). To appear in ENTCS, 2004}, OPTpages = {}, year = {2004}, OPTeditor = {}, OPTvolume = {}, OPTnumber = {}, OPTseries = {}, OPTaddress = {}, OPTmonth = {}, OPTorganization = {}, OPTpublisher = {}, OPTnote = {}, OPTannote = {} } % Theme H. Resource models and web data % and/or % Theme D. Specification and verification methods @InProceedings{BCOP05, author = {Bornat and Calcagno and O'Hearn and Parkinson}, title = {Permission Accounting in Separation Logic}, OPTcrossref = {}, OPTkey = {}, booktitle = {Proceedings of POPL 2005: The 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Long Beach)}, OPTpages = {}, year = {2005}, OPTeditor = {}, OPTvolume = {}, OPTnumber = {}, OPTseries = {}, OPTaddress = {}, OPTmonth = {}, OPTorganization = {}, OPTpublisher = {}, note = {To appear}, OPTannote = {} } %Theme H. Resource models and web data %and/or %Theme D. Specification and verification methods @InProceedings{PB05, author = {Parkinson and Bierman}, title = {Separation logic and abstraction}, OPTcrossref = {}, OPTkey = {}, booktitle = {Proceedings of POPL 2005: The 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Long Beach)}, OPTpages = {}, year = {2005}, OPTeditor = {}, OPTvolume = {}, OPTnumber = {}, OPTseries = {}, OPTaddress = {}, OPTmonth = {}, OPTorganization = {}, OPTpublisher = {}, note = {To appear}, OPTannote = {} } % Theme H. Resource models and web data @PhdThesis{Serjantov-thesis, author = {Andrei Serjantov}, title = {On the Anonymity of Anonymity Systems}, school = {University of Cambridge}, year = {2004}, OPTkey = {}, OPTtype = {}, OPTaddress = {}, OPTmonth = {}, OPTnote = {}, OPTannote = {} } % Theme H. Resource models and web data @InProceedings{DGG04, author = {Anuj Dawar and Philippa Gardner and Giorgio Ghelli}, title = {Adjunct Elimination Through Games in Static Ambient Logic}, booktitle = {FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science: 24th International Conference}, pages = {211-223}, year = {2004}, series = {LNCS}, volume = {3328}, publisher = {Springer} } % Theme B. @Article{PittsAM:monsf, author = {M. R. Shinwell and A. M. Pitts}, title = {On a Monadic Semantics for Freshnes}, journal = {Theoretical Computer Science}, year = {200X}, note = {to appear. A preliminary version appears in the proceedings of the Second workshop of the EU FP5 IST thematic network IST-2001-38957 APPSEM II, Tallinn, Estonia, April 2004} } % Theme G. Semantic methods for distributed computing @InProceedings{VVW04, author = {Varacca and Voelzer and Winskel}, title = { Probabilistic event structures and domains }, OPTcrossref = {}, OPTkey = {}, booktitle = { In CONCUR'04. Springer LNCS}, OPTpages = {}, year = {2004}, OPTeditor = {}, OPTvolume = {}, OPTnumber = {}, OPTseries = {}, OPTaddress = {}, OPTmonth = {}, OPTorganization = {}, OPTpublisher = {}, OPTnote = {}, OPTannote = {} } % Theme G. Semantic methods for distributed computing @InProceedings{WZ04, author = {Winskel and Zappa Nardelli}, title = { new-HOPLA: a higher-order process language with name generation }, OPTcrossref = {}, OPTkey = {}, booktitle = {TCS@2004, Third IFIP International Conference on Theoretical Computer Science, 2004, Kluwer}, OPTpages = {}, year = {2004}, OPTeditor = {}, OPTvolume = {}, OPTnumber = {}, OPTseries = {}, OPTaddress = {}, OPTmonth = {}, OPTorganization = {}, OPTpublisher = {}, OPTnote = {}, OPTannote = {} } % Theme G. Semantic methods for distributed computing @InJournal{CW04, author = {Cattani and Winskel}, title = {Profunctors, Open Maps and Bisimulation }, OPTcrossref = {}, OPTkey = {}, booktitle = {Mathematical Structures in Computer Science }, OPTpages = {}, year = {2004}, OPTeditor = {}, OPTvolume = {}, OPTnumber = {}, OPTseries = {}, OPTaddress = {}, OPTmonth = {}, OPTorganization = {}, OPTpublisher = {}, OPTnote = {Accepted, to appear}, OPTannote = {} } % Theme G. Semantic methods for distributed computing @InJournal{NW04, author = {Nygaard and Winskel}, title = { Domain Theory for Concurrency }, OPTcrossref = {}, OPTkey = {}, booktitle = {Theoretical Computer Science, 316(1) }, OPTpages = {}, year = {2004}, OPTeditor = {}, OPTvolume = {}, OPTnumber = {}, OPTseries = {}, OPTaddress = {}, OPTmonth = {}, OPTorganization = {}, OPTpublisher = {}, OPTnote = {}, OPTannote = {} }@TechReport{norell:lic, author = {Ulf Norell}, title = {Implementing Functional Generic Programming}, institution = {Chalmers University}, year = 2004 } @InProceedings{norell-jansson:mpc, author = {Ulf Norell and Patrik Jansson}, title = {Prototyping Generic Programming using Template Haskell}, booktitle = {Seventh International Conference on Mathematics of Program Construction}, year = 2004, publisher = {Springer Verlag} } @InProceedings{danielsson-jansson:mpc, author = {Nils Anders Danielsson and Patrik Jansson}, title = {Chasing Bottoms, A Case Study in Program Verification in the Presence of Partial and Infinite Values.}, booktitle = {Proceedings of the 7th International Conference on Mathematics of Program Construction}, year = 2004, publisher = {Springer Verlag} } @InProceedings{dybjer-qiao-takeyama:guiyang, title = {Random generators for dependent types}, year = 2004, booktitle = {Proceedings of the First International Colloquium on Theoretical Aspects of Computing, Guiyang, China,} } @Article{dybjer-qiao-takeyama:ist, author = {Peter Dybjer and {Qiao Haiyan} and Makoto Takeyama}, title = {Verifying Haskell programs by combining testing, model checking and interactive theorem proving}, journal = {Information and Software Technology}, year = 2004 } @InProceedings{claessen-martensson:fmcad, author = {Koen Claessen and Johan M\aa rtensson}, title = {An Operational Semantics for Weak PSL}, booktitle = {FMCAD}, year = 2004 } @Article{claessen:jfp, author = {Koen Claessen}, title = {Parallel Parsing Processes}, journal = {Journal of Functional Programming}, year = 2004, note = {Accepted for publication} } @InProceedings{abel-matthes:csl, author = {Andreas Abel and Ralph Matthes}, title = {Fixed Points of Type Constructors and Primitive Recursion}, booktitle = {Computer Science Logic, 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL}, year = 2004, publisher = {Springer} } @Article{abel:rairo, author = {Andreas Abel}, title = {Termination Checking with Types}, journal = {RAIRO - Theoretical Informatics and Applications}, year = 2004, volume = 38, number = 4, pages = {277-319} } @InProceedings{abel:ijcar, author = {Andreas Abel}, title = {Weak Normalization for the Simply-Typed lambda-calculus in Twelf}, booktitle = {Logical Frameworks and Metalanguages (LFM 04), IJCAR, Cork, Ireland}, year = 2004 } @InProceedings{aehss2004b, author = {Jesper Andersen and Ebbe Elsborg and Fritz Henglein and Jakob Grue Simonsen and Christian Stefansen}, title = {Compositional Specification of Commercial Contracts}, year = {2004}, booktitle = {Proceedings of the 1st International Symposium on Leveraging Applications of Formal Methods (ISOLA '04)}, publisher = {}, pages = {}, theme = {CE}, deliverable = {D13}, site = {copenhagen} } @InProceedings{BirkedalL:bigpl, author = {L. Birkedal}, title = {Bigraphical Programming Languages}, booktitle = {In Proceedings of 2nd UK UbiNet Workshop}, year = 2004, address = {Cambridge, UK}, month = {May}, note = {Position Paper}, theme = {G}, deliverable = {D13}, site = {copenhagen} } @inproceedings{BirkedalL:bihsl, author = {Bodil Biering and Lars Birkedal and Noah Torp-Smith}, title = {BI Hyperdoctrines and Higher-Order Separation Logic.}, booktitle = {ESOP}, year = {2005}, pages = {233-247}, ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3444{\&}spage=233}, crossref = {DBLP:conf/esop/2005}, bibsource = {DBLP, http://dblp.uni-trier.de} } @TechReport{BirkedalL:defp-tr, author = {L. Birkedal and R.E. Møgelberg}, title = {On the Definition of Parametricity}, institution = {The IT University of Copenhagen}, year = 2004, number = 44, theme = {E}, deliverable = {D13}, site = {copenhagen} } @Proceedings{BirkedalL:recddt, title = {Recent Developments in Domain Theory}, year = 2004, editor = {L. Birkedal and M. Escardo and A. Jung and G. Rosolini}, series = {Theoretical Computer Science}, publisher = {Elsevier}, theme = {EFG}, deliverable = {D13}, site = {copenhagen} } @InProceedings{BirkedalL.locrcg} author = {L. Birkedal and N. Torp-Smith and J.C. Reynolds}, title = {Local Reasoning about a Copying Garbage Collector}, booktitle = {Proc.\ 31-st ACM SIGPLAN-SIGACT Symp.\ on Principles of Programming Languages (POPL)}, year = {2004}, publisher = {ACM Press}, month = {January}, pages = {220--231}, theme = {EF}, deliverable = {D13}, site = {copenhagen} } @Article{BirkedalL:regmmp, author = {M. Tofte and L. Birkedal and M. Elsman and N. Hallenberg}, title = {A Retrospective on Region-based Memory Management}, journal = {Higher-order Symbolic Computation}, year = 2004, volume = 17, number = 2, theme = {EF}, deliverable = {D13}, site = {copenhagen} } @Article{ChristensenGlueck:04:ONOFF, AUTHOR = {Christensen, Niels H. and Glück, Robert}, YEAR = {2004}, TITLE = {Offline Partial Evaluation can be as Accurate as Online Partial Evaluation}, JOURNAL = {{ACM} Transactions on Programming Languages and Systems}, volume = {26}, number = {1}, pages = {191--220}, keywords = {binding-time analysis, constant propagation, generalization, offline partial evaluation, online partial evaluation, metacomputation, program specialization}, summary = {We show that the accuracy of online partial evaluation, or polyvariant specialization based on constant propagation, can be simulated by offline partial evaluation using a maximally polyvariant binding-time analysis. We point out that, while their accuracy is the same, online partial evaluation offers better opportunities for powerful generalization strategies. Our results are presented using a flowchart language with recursive procedures.}, URL = {http://doi.acm.org/10.1145/963778.963784}, SEMNO = {D-503}, PUF = {Artikel optaget i tidsskrift}, ID = {Art2}, theme = {C}, deliverable = {D13}, site = {copenhagen} } @InProceedings{Debois:2004:imperative, AUTHOR = {Søren Debois}, YEAR = {2004}, TITLE = {Imperative Program Optimization by Partial Evaluation}, BOOKTITLE = {Proceedings of the 2004 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM '04)}, publisher = {The ACM Press}, pages = {113 -- 122}, theme = {C}, deliverable = {D13}, site = {copenhagen} } @InProceedings{Filinski-Rohde:FOSSACS04, AUTHOR = {Filinski, Andrzej and Rohde, Henning Korsholm}, YEAR = 2004, TITLE = {A Denotational Account of Untyped Normalization by Evaluation}, BOOKTITLE = {7th International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2004)}, editor = {Igor Walukiewicz}, publisher = {Springer-Verlag}, address = {Barcelona, Spain}, series = LNCS, volume = 2987, pages = {167-181}, month = Mar, abstract = { We show that the standard normalization-by-evaluation construction for the simply-typed $\lambda_{\beta\eta}$-calculus has a natural counterpart for the untyped $\lambda_\beta$-calculus, with the central type-indexed logical relation replaced by a ``recursively defined'' \emph{invariant relation}, in the style of Pitts. In fact, the construction can be seen as generalizing a computational-adequacy argument for an untyped, call-by-name language to normalization instead of evaluation. In the untyped setting, not all terms have normal forms, so the normalization function is necessarily partial. We establish its correctness in the senses of \emph{soundness} (the output term, if any, is $\beta$-equivalent to the input term); \emph{standardization} ($\beta$-equivalent terms are mapped to the same result); and \emph{completeness} (the function is defined for all terms that do have normal forms). We also show how the semantic construction enables a simple yet formal correctness proof for the normalization algorithm, expressed as a functional program in an ML-like call-by-value language.}, theme = {C}, deliverable = {D13}, site = {copenhagen} } @InProceedings{GlueckKawabe:04:LRinv, AUTHOR = {Glück, Robert and Kawabe, Masahiko}, YEAR = {2004}, TITLE = {Derivation of deterministic inverse programs based on {LR} parsing}, BOOKTITLE = {Functional and Logic Programming. Proceedings}, editor = {Kameyama, Yukiyoshi and Stuckey, Peter J.}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2998}, pages = {291--306}, keywords = {program inversion, functional programming, program transformation, LR parsing}, summary = {We present a method for automatic program inversion of functional programs based on methods of LR parsing. We formalize the transformation and illustrate it with the inversion of a program for run-length encoding. We solve one of the main problems of automatic program inversion---the elimination of nondeterminism---by viewing an inverse program as a context-free grammar and applying to it methods of LR parsing to turn it into a recursive, deterministic inverse program. This improves the efficiency of the inverse programs and greatly expands the application range of our earlier method for program inversion.}, URL = {http://www.springerlink.com/link.asp?id=tfaxx9x8mxukcreb}, SEMNO = {D-506}, PUF = {Artikel i proceedings (med censur)}, ID = {KonR}, theme = {C}, deliverable = {D13}, site = {copenhagen} } @InProceedings{JonesBohr:04:lambda-termination, AUTHOR = {Jones, N.D and Bohr, Nina}, YEAR = {2004}, TITLE = {Termination Analysis of the Untyped $\lambda$-Calculus}, BOOKTITLE = {Rewriting Techniques and Applications. Proceedings}, editor = {van Oostrom, V.}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {3091}, pages = {1--23}, summary = {}, URL = {}, theme = {C}, deliverable = {D13}, site = {copenhagen} } @Article{ peval-termination-jones-glenstrup, AUTHOR = {Jones, N.D. and Glenstrup, A.}, YEAR = {2004}, TITLE = {Partial Evaluation Termination Analysis and Specialization-Point Insertion}, JOURNAL = {ACM Transactions on Programming Languages and Systems}, OPTvolume = {?}, number = {}, pages = {101}, month = {}, keywords = {}, summary = { Recent research suggests that the goal of fully automatic and reliable program generation for a broad range of applications is coming nearer to feasibility. Although the goal of fully automatic program generation is still far from fully achieved, there has been some success in a special case: partial evaluation, also known as program specialization. A key problem in all program generation is {\em termination} of the generation process. This paper describes recent progress towards automatically solving the termination problem, first for individual programs, and then for specializers and ``generating extensions,'' the program generators that most offline partial evaluators produce.}, theme = {C}, deliverable = {D13}, site = {copenhagen} } @Article{ compiler-correct-jones-et-al, AUTHOR = {Lacey, D. and Jones, N.D. and Van Wyk, E. and Frederiksen, C.C.}, YEAR = {2004}, TITLE = {Compiler optimization correctness by temporal logic}, JOURNAL = {Higher Order and Symbolic Computation}, volume = {17}, number = {3}, pages = {173--206}, summary = {Rewrite rules with side conditions of form: $I \Rightarrow I' {\rm if} \phi$ can elegantly express many classical compiler optimizations for imperative programming languages. In this paper, programs are written in an intermediate language and transformation-enabling side conditions are specified in a temporal logic suitable for describing program data flow. The purpose of this paper is to show how such transformations may be proven correct. Our methodology is illustrated by three familiar optimizations: dead code elimination, constant folding, and code motion. A transformation is correct if whenever it can be applied to a program, the original and transformed programs are semantically equivalent, i.e., they compute the same input-output function. The proofs of semantic equivalence inductively show that a transformation-specific bisimulation relation holds between the original and transformed program computations.}, theme = {C}, deliverable = {D13}, site = {copenhagen} } @Article{ interpreter-spec-jones, AUTHOR = {Jones, N.D.}, YEAR = {2004}, TITLE = {Transformation by interpreter specialisation}, JOURNAL = {Science of Computer Programming}, volume = {52}, pages = {307--339}, summary = {A program may be transformed by specialising an interpreter for the language in which it is written. Efficiency of the transformed program is determined by the efficiency of the interpreter's dynamic operations; the efficiency of its static operations is irrelevant, since all will be ``specialised away''. This approach is {\em automatic} (as automatic as the specialiser is); {\em general}, in that it applies to all of the interpreter's input programs; and {\em flexible}, in that a wide range of program transformations are achievable since the transformed program inherits the style of the interpreter. The chief practical challenge is understanding cause and effect: How should one write the interpreter so that specialisation produces efficient transformed programs? The core of this paper is a series of examples, both positive and negative, showing how the way the interpreter is written can influence the removal of interpretational overhead, and thus the efficiency and size of the target programs obtained by specialisation.}, theme = {C}, deliverable = {D13}, site = {copenhagen} } @InProceedings{lawall:gpce04, AUTHOR = {Julia L. Lawall and Anne-Fran\c{c}oise Le Meur and Gilles Muller}, YEAR = {2004}, TITLE = {On Designing a Target-Independent DSL for Safe OS Process-Scheduling Components}, BOOKTITLE = {Third International Conference on Generative Programming and Component Engineering (GPCE'04)}, editor = {Gabor Karsai and Eelco Visser}, publisher = {Springer}, organization = {}, address = {Vancouver, Canada}, series = {Lecture Notes in Computer Science}, volume = {3286}, pages = {436--455}, month = {October}, keywords = {process scheduling, domain-specific languages, verification}, summary = {Developing new process-scheduling components for multiple OSes is challenging because of the tight interdependence between an OS and its scheduler and because of the stringent safety requirements that OS code must satisfy. In this context, a domain-specific language (DSL), designed by a scheduling expert, can encapsulate scheduling expertise and thus facilitate scheduler programming and verification. Nevertheless, designing a DSL that is target-independent and provides safety guarantees requires expertise not only in scheduling but also in the structure of various OSes. To address these issues, we propose the introduction of an OS expert into the DSL design process and the use of a type system to enable the OS expert to express relevant OS properties. This paper instantiates our approach in the context of the Bossa process-scheduling framework and describes how the types provided by an OS expert are used to ensure that Bossa scheduling components are safe. }, theme = {CD}, deliverable = {D13}, site = {copenhagen} } @InProceedings{lawall:plos04, AUTHOR = {Julia L. Lawall and Anne-Fran\c{c}oise Le Meur and Gilles Muller}, YEAR = {2004}, TITLE = {Modularity for the Bossa Process-Scheduling Language}, BOOKTITLE = {ECOOP Workshop on Programming Languages and Operating Systems (ECOOP-PLOS 2004)}, editor = {}, publisher = {}, organization = {}, address = {Oslo, Norway}, series = {Technical report TR-ICS-04-22, Donald Bren School of Information and Computer Science, University of California, Irvine}, volume = {}, pages = {1--5}, month = {June}, keywords = {}, summary = {Bossa is a framework for implementing scheduling policies in standard operating systems. This frame­work provides a domain-specific language that eases the specification of scheduling policies and enables verification of critical safety properties. In previous work we have specified the semantics of the Bossa language and the verification process. In this work, we propose a modular version of the language, to take advantage of the many opportunities for code reuse and modularity provided by scheduling policies. }, theme = {A}, deliverable = {D13}, site = {copenhagen} } @Article{lawall:scp04, AUTHOR = {Charles Consel and Julia L. Lawall and Anne-Fran\c{c}oise Le Meur}, YEAR = {2004}, TITLE = {A Tour of Tempo: a Program Specializer for the C language}, JOURNAL = {Science of Computer Programming}, volume = {52}, number = {}, pages = {341--370}, month = {}, keywords = {}, summary = { Specialization is an automatic approach to customizing a program with respect to configuration values. In this paper, we present a survey of Tempo, a specializer for the C language. Tempo offers specialization at both compile time and run time, and both program and data specialization. To control the specialization process, Tempo provides the program developer with a declarative language to describe specialization opportunities for a given program. The functionalities and features of Tempo have been driven by the needs of practical applications. Tempo has been successfully applied to a variety of realistic programs in areas such as operating systems and networking. We give an overview of the design of Tempo and of its use in specializing realistic applications. }, theme = {C}, deliverable = {D13}, site = {copenhagen} } @Article{lawall:hosc04, AUTHOR = {Anne-Fran\c{c}oise Le Meur and Julia L. Lawall and Charles Consel}, YEAR = {2004}, TITLE = {A Pragmatic Approach to Declaring Specialization Scenarios}, JOURNAL = {Higher-Order and Symbolic Computation}, volume = {17}, number = {1}, pages = {47--92}, month = {March}, keywords = {}, summary = {Partial evaluation is a program transformation that automatically specializes a program with respect to invariants. Despite successful application in areas such as graphics, operating systems, and software engineering, partial evaluators have yet to achieve widespread use. One reason is the difficulty of adequately describing specialization opportunities. Indeed, underspecialization or overspecialization often occurs, without any feedback as to the source of the problem. We have developed a high-level, module-based language allowing the program developer to guide the choice of both the code to specialize and the invariants to exploit during the specialization process. To ease the use of partial evaluation, the syntax of this language is similar to the declaration syntax of the target language of the partial evaluator. To provide feedback, declarations are checked during the analyses performed by partial evaluation. The language has been successfully used by a variety of users, including students having no previous experience with partial evaluation. }, theme = {C}, deliverable = {D13}, site = {copenhagen} } @InProceedings{glabbeek/plotkin:resolvable-conflict, author = {Rob van Glabbeek and Gordon Plotkin}, title = {Event Structures for Resolvable Conflict}, booktitle = {Mathematical Foundations of Computer Science 2004: Proceedings of the 29th International Symposium MFCS~2004}, pages = {550--561}, year = 2004, series = {Lecture Notes in Computer Science~3153}, publisher = {Springer-Verlag}, pdf = {http://homepages.inf.ed.ac.uk/gdp/publications/resolv.pdf}, url = {http://www.springerlink.com/link.asp?id=jypn558pu4kxqx47}, theme = {G}, site = {edinburgh} } @Unpublished{glabbeek/plotkin:configuration-structures-petri-nets, author = {Rob van Glabbeek and Gordon Plotkin}, title = {Configuration Structures, Event Structures and {Petri} Nets}, note = {Journal article, in preparation}, year = 2004, pdf = {http://www.cse.unsw.edu.au/~rvg/epsrcGR/S22097/conf.pdf}, theme = {G}, site = {edinburgh} } @InProceedings{glabbeek:express-hd-automata, author = {Rob van Glabbeek}, title = {On the Expressiveness of Higher Dimensional Automata}, booktitle = {EXPRESS~'04: Proceedings of the 11th Workshop on Expressiveness in Concurrency}, year = 2004, series = {Electronic Notes in Theoretical Computer Science}, publisher = {Elsevier}, pdf = {http://www.cse.unsw.edu.au/~rvg/hda.pdf}, theme = {G}, site = {edinburgh} } @Unpublished{glabbeek/plotkin:st-configuration, author = {Rob van Glabbeek and Gordon Plotkin}, title = {Configuration Structures for Impurity, Preliminary Draft}, note = {Available online}, year = 2004, pdf = {http://www.cse.unsw.edu.au/~rvg/epsrcGR/S22097/st-conf.pdf}, theme = {G}, site = {edinburgh} } @Unpublished{glabbeek/plotkin:equivalence-notions-petri-nets, author = {Rob van Glabbeek and Gordon Plotkin}, title = {Equivalence Notions for {Petri} Nets and Configuration Structures, Preliminary Notes}, note = {Available online}, year = 2004, pdf = {http://www.cse.unsw.edu.au/~rvg/epsrcGR/S22097/st-conf.pdf}, theme = {G}, site = {edinburgh} } @Unpublished{tix+:semantic-domains-prob-nondet, author = {Regina Tix and Klaus Keimel and Gordon Plotkin}, title = {Semantic Domains for Combining Probability and Non-Determinism}, note = {Draft available online}, ps = {http://homepages.inf.ed.ac.uk/gdp/publications/tkp.ps}, url = {http://homepages.inf.ed.ac.uk/gdp/publications/}, theme = {I}, site = {edinburgh,darmstadt} } @Article{hyland+:combining-effects, author = {Martin Hyland and Gordon Plotkin and John Power}, title = {Combining Effects: Sum and Tensor}, journal = {Theoretical Computer Science}, year = 2004, pdf = {http://homepages.inf.ed.ac.uk/gdp/publications/Comb_Effects_Jour.pdf}, url = {http://homepages.inf.ed.ac.uk/gdp/publications/}, OPTtheme = {?}, site = {edinburgh,cambridge} } @Unpublished{plotkin/power:logic-computational-effects, author = {Gordon Plotkin and John Power}, title = {Logic for Computational Effects: Work in Progress}, note = {Available online}, year = 2004, pdf = {http://homepages.inf.ed.ac.uk/gdp/publications/logic_outline.pdf}, url = {http://homepages.inf.ed.ac.uk/gdp/publications/}, OPTtheme = {?}, site = {edinburgh} } @InProceedings{hyland+:combining-continuations-other-effects, author = {Martin Hyland and Blain Levy, Paul and Gordon Plotkin and John Power}, title = {Combining Continuations with Other Effects}, booktitle = {Proceedings of the Fourth ACM SIGPLAN Continuations Workshop~CW~'04}, month = jan, year = 2004, pdf = {http://www.cs.bham.ac.uk/~hxt/cw04/hyland.pdf}, OPTtheme = {?}, site = {edinburgh,cambridge,birmingham} } @InProceedings{longley/pollack:reasoning-about-cbv, author = {John Longley and Randy Pollack}, title = {Reasoning About {CBV} Functional Programs in {Isabelle/HOL}}, booktitle = {Theorem Proving in Higher Order Logics: Proceedings of the 17th International Conference TPHOLs 2004}, year = 2004, ps = {http://homepages.inf.ed.ac.uk/rap/export/LongleyPollack04.ps.gz}, url = {http://homepages.inf.ed.ac.uk/rap/}, theme = {BD}, site = {edinburgh} } @InProceedings{katsumata:generalisation-prelogical-predicates, author = {Shin-ya Katsumata}, title = {A Generalisation of Prelogical Predicates to Simply Typed Formal Systems}, booktitle = {Automata, Languages and Programming: Proceedings of the 31st International Colloquium ICALP~2004}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science~3142}, pages = {831--845}, year = 2004, pdf = {http://www.kurims.kyoto-u.ac.jp/~sinya/paper/generalpre.pdf}, url = {http://www.kurims.kyoto-u.ac.jp/~sinya/paper/}, abstract = {We generalise the notion of prelogical predicates to arbitrary simply typed formal systems and their categorical models. We establish the basic lemma of prelogical predicates and composability of binary prelogical relations in this generalised setting. This generalisation takes place in a framework for typed higher-order abstract syntax and semantics.}, theme = {D}, site = {edinburgh} } @InCollection{sannella:casl-semantics04, editor = {Donald Sannella and Andrzej Tarlecki}, title = {{CASL} Semantics}, booktitle = {CASL Reference Manual}, publisher = {Springer}, part = {III}, bookeditor = {Peter Mosses}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science~2690}, pages = {115--274}, year = 2004, theme = {D}, site = {edinburgh} } @InProceedings{sannella:casl-refinement04, author = {Till Mossakowski and Donald Sannella and Andrzej Tarlecki}, title = {A Simple Refinement Language for {CASL}}, booktitle = {Recent Trends in Algebraic Development Techniques: Selected Papers from WADT~2004}, location = {Barcelona}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, year = 2004, abstract = {We extend CASL architectural specifications with a simple refinement language that allows the formalization of developments as refinement trees. The essence of the extension is to allow refinements of unit specifications in CASL architectural specifications.}, theme = {D}, site = {edinburgh} } @InProceedings{aspinall+:mrg-overview-cassis, author = {David Aspinall and Stephen Gilmore and Martin Hofmann and Donald Sannella and Ian Stark}, title = {Mobile Resource Guarantees for Smart Devices}, booktitle = {Proceedings of the International Workshop on Construction and Analysis of Safe, Secure and Interoperable Smart Devices CASSIS~2004}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, year = 2004, abstract = {We present the Mobile Resource Guarantees framework: a system for ensuring that downloaded programs are free from run-time violations of resource bounds. Certificates are attached to code in the form of efficiently checkable proofs of resource bounds; in contrast to cryptographic certificates of code origin, these are independent of trust networks. A novel programming language with resource constraints encoded in function types is used to streamline the generation of proofs of resource usage.}, theme = {I}, site = {edinburgh,munich} } @InProceedings{aspinall+:program-logic-resource-verification, author = {David Aspinall and Lennart Beringer and Martin Hofmann and Hans-Wolfgang Loidl and Alberto Momigliano}, title = {A Program Logic for Resource Verification}, booktitle = {Theorem Proving in Higher Order Logics: Proceedings of the 17th International Conference TPHOLs 2004}, year = 2004, series = {Lecture Notes in Computer Science~3223}, publisher = {Springer-Verlag}, pdf = {http://groups.inf.ed.ac.uk/mrg/publications/mrg/tphol-paper.pdf}, url = {http://homepages.inf.ed.ac.uk/da/papers/tphols04/}, theme = {I}, site = {edinburgh,munich} } @InProceedings{beringer+:towards-certificate-generation, author = {Lennart Beringer and Martin Hofmann and Alberto Momigliano and Olha Shkaravska}, title = {Towards Certificate Generation for Linear Heap Consumption}, booktitle = {Proceedings of the ICALP/LICS Workshop on Logics for Resources, Processes, and Programs LRPP~2004}, year = 2004, pdf = {http://groups.inf.ed.ac.uk/mrg/publications/mrg/lrpp.pdf}, url = {http://homepages.inf.ed.ac.uk/amomigl1/#Papers}, theme = {I}, site = {edinburgh,munich} } @PhdThesis{lindley:thesis, author = {Samuel Lindley}, title = {Normalisation by Evaluation in the Compilation of Typed Functional Programming Languages}, school = {University of Edinburgh}, year = 2004, note = {Submitted}, pdf = {http://www.dcs.ed.ac.uk/home/samuel/Thesis/thesis_submitted.pdf}, url = {http://www.dcs.ed.ac.uk/home/samuel/Papers/}, theme = {C}, site = {edinburgh} } @InProceedings{benton+:shrinking-reductions-sml-net, author = {Nick Benton and Andrew Kennedy and Sam Lindley and Claudio Russo}, title = {Shrinking Reductions in {SML.NET}}, booktitle = {Proceedings of the 16th International Workshop on Implementation and Application of Functional Languages IFL~'04}, year = 2004, note = {Draft proceedings, Technical Report 0408, Institute of Computer Science and Applied Mathematics, University of Kiel}, pdf = {http://www.dcs.ed.ac.uk/home/samuel/Papers/shrinking.pdf}, url = {http://www.dcs.ed.ac.uk/home/samuel/Papers/}, theme = {C}, site = {edinburgh,microsoft} } @Unpublished{lindley/stark:reducibility-tt-computation-types, author = {Samuel Lindley and Ian Stark}, title = {Reducibility and TT-lifting for Computation Types }, note = {Submitted for publication}, year = 2004, pdf = {http://www.dcs.ed.ac.uk/home/samuel/Papers/reducibility.pdf}, url = {http://www.dcs.ed.ac.uk/home/samuel/Papers/}, theme = {BD}, site = {edinburgh} } @InProceedings{abramsky+:nominalgames, author = {Samson Abramsky and Dan Ghica and Andrzej Murawski and Luke Ong and Ian Stark}, title = {Nominal Games and Full Abstraction for the Nu-Calculus}, booktitle = {Proceedings of the Nineteenth Annual IEEE Symposium on Logic in Computer Science}, pages = {150--159}, year = 2004, publisher = {IEEE Computer Society Press}, url = {http://www.ed.ac.uk/~stark/nominalgames.html}, pdf = {http://www.ed.ac.uk/~stark/nominalgames.pdf}, theme = {F}, site = {edinburgh,oxford} } @InProceedings{schoepp/stark:names+binding, author = {Ulrich {Sch\"opp} and Ian Stark}, title = {A Dependent Type Theory with Names and Binding}, booktitle = {Computer Science Logic: Proceedings of the 18th International Workshop CSL~2004}, pages = {235--249}, year = 2004, series = {Lecture Notes in Computer Science~3210}, publisher = {Springer-Verlag}, url = {http://www.ed.ac.uk/~stark/bunches.html}, pdf = {http://www.ed.ac.uk/~stark/names+binding.pdf}, theme = {BDEH}, site = {edinburgh} } @Unpublished{stark:free-algebra-models-pi, author = {Ian Stark}, title = {Free-Algebra Models for the $\pi$-Calculus}, note = {Submitted for publication}, year = 2004, theme = {G}, site = {edinburgh} } @Article{wadler:girard-reynolds-iso-2, author = {Philip Wadler}, title = {The Girard-Reynolds isomorphism (second edition)}, journal = {Theoretical Computer Science}, year = 2004, note = {To appear}, pdf = {http://homepages.inf.ed.ac.uk/wadler/papers/gr2/gr2.pdf}, url = {http://homepages.inf.ed.ac.uk/wadler/topics/parametricity.html#gr2}, theme = {BDE}, site = {edinburgh} } @Article{simpson:recursive, author = {Alex Simpson}, title = {Computational Adequacy for Recursive Types in Models of Intuitionistic Set Theory}, journal = {Annals of Pure and Applied Logic}, volume = 130, pages = {207--275}, year = 2004, pdf = {http://homepages.inf.ed.ac.uk/als/Research/cartinmist.pdf}, url = {http://homepages.inf.ed.ac.uk/als/Research/}, theme = {EI}, site = {edinburgh} } @Article{simpson:hennessy-milner, author = {Alex Simpson}, title = {Sequent Calculi for Process Verification: {Hennessy-Milner} Logic for an Arbitrary {GSOS}}, journal = {Journal of Logic and Algebraic Programming}, volume = {60--61}, pages = {287--322}, year = 2004, pdf = {http://homepages.inf.ed.ac.uk/als/Research/scpv.pdf}, url = {http://homepages.inf.ed.ac.uk/als/Research/}, theme = {BCDG}, site = {edinburgh} } @Article{escardo-lawson-simpson, author = {Mart{\'i} Escardó and Jimmie Lawson and Alex Simpson}, title = {Comparing Cartesian-closed Categories of (Core) Compactly Generated Spaces}, journal = {Topology and its Applications}, volume = 143, pages = {105--145}, year = 2004, theme = {I}, site = {edinburgh,birmingham} } @Article{bauer-simpson, author = {Andrej Bauer and Alex Simpson}, title = {Two Constructive Embedding-Extension Theorems with Applications to Continuity Principles and to Banach-Mazur Computability}, journal = {Mathematical Logic Quarterly}, pages = {351--369}, volume = 50, year = 2004, theme = {I}, site = {edinburgh} } {Article{kick-power-simpson, author = {Marco Kick and John Power and Alex Simpson}, title = {Coalgebraic Semantics for Timed Processes}, journal = {Information and Computation}, volume = {To appear}, year = 2005, theme = {GHI}, site = {edinburgh} } @InProceedings{atkey04lambdasep, author = {Robert Atkey}, title = {A $\lambda$-Calculus for Resource Separation}, booktitle = {Automata, Languages and Programming: Proceedings of the 31st International Colloquium ICALP~2004}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science~3142}, pages = {158--170}, year = 2004, pdf = {http://homepages.inf.ed.ac.uk/s9720988/lambda-sep-icalp.pdf}, url = {http://homepages.inf.ed.ac.uk/s9720988/}, theme = {EH}, site = {edinburgh} } @string{acm="ACM Press"} @string{kl="Kluwer Academic Publishers"}@string{popl04="ACM Symp. on Principles of Programming Languages 2004"} @string{oops04="ACM Symp. on Applied Computing (SAC 2004), Special Track on Object-Oriented Programming Languages and Systems"} @InProceedings{Anc+Mog:GPCE-2004, author = {D. Ancona and E. Moggi}, title = {A Fresh Calculus for Names Management}, pdf= {http://www.disi.unige.it/person/MoggiE/ftp/gpce04.pdf}, crossref = {GPCE2004}, abstract={ We define a basic calculus $ML^N$ for manipulating symbolic names inspired by both the $\nu^Box$ calculus of Nanevski and Pfenning and the $CMS$ calculus of Ancona and Zucca. The resulting calculus provides a smooth integration of the peculiar features of $\nu^Box$ and $CMS$, namely the use of symbolic names for meta-programming and programming in-the-large, and overcomes several deficiencies of these two calculi. We present two different extensions of the basic calculus, the first consider the interaction between linking and computational effects (in the form of imperative computations), the second shows how $CMS$ can be naturally encoded into $ML^N$. A posteriori the calculus appears related to $\lambda$-calculi with extensible records, and able to model some aspects of the mechanism of Java class loaders. }, theme = {AC}, workpackage = {1}, site = {genova}} @InProceedings{Cal+Mog+Tah:ESOP-2004, author = {C. Calcagno and E. Moggi and W. Taha}, title = {{ML}-like Inference for Classifiers}, crossref = {ESOP2004}, pdf= {http://www.disi.unige.it/person/MoggiE/ftp/CMT03-sub.pdf}, abstract={ Environment classifiers were recently proposed as a new approach to typing multi-stage languages. Safety was established in the simply-typed and let-polymorphic settings. While the motivation for the classifier approach was the feasibility of inference, this was in fact not established. This paper starts with the observation that inference for the full classifier-based system fails. We then identify a subset of the original system for which inference is possible. This subset, which uses {implicit classifiers}, retains significant expressivity (e.g. it can embed the calculi of Davies and Pfenning) and eliminates the need for classifier names in terms. Implicit classifiers were implemented in MetaOCaml, and no changes were needed to make an existing test suite acceptable by the new type checker. }, theme = {CE}, workpackage = {2}, site = {genova}} @Proceedings{GPCE2004, title = {Generative Programming and Component Engineering}, OPTbooktitle = {Generative Programming and Component Engineering}, series = LNCS, publisher = SV, volume = 3286, month = Oct, year = 2004, xaddress = {Vancouver}, editor = {G. Karsai and E. Visser}, }, } @string{ESOP2004 = {Programming Languages \& Systems, 13th European Symp.\ Programming}} @Proceedings{ESOP2004, title = ESOP2004, booktitle = ESOP2004, key = {ES{\relax OP} '04}, year = 2004, series = LNCS, volume = 2986, publisher = SV, xdate = {2004-03-29/--04-02}, xpublisher = {Springer-Verlag Berlin and Heidelberg GmbH & Co. KG}, xaddress = {Barcelona, Spain}, xnote = {held as part of ETAPS 2004}, xeditor = {David Schmidt}, isbn = {3-540-21313-9}, } @InProceedings{Lagorio04, editor = {Hisham Haddad and Andrea Omicini and Roger L. Wainwright and Lorie M. Liebrock}, booktitle = oops04, author = "G. Lagorio", title = "Another Step Towards a Smart Compilation Manager for {J}ava", publisher = acm, month={March}, year = 2004, isbn = {1-58113-812-1}, pages = {1275--1280}, theme = {E}, workpackage = {1}, site = {genova}} @Article{Lagorio04a, author = "G. Lagorio", title = "{C}apturing ghost dependencies in {J}ava sources", journal = "Journal of Object Technology", year = 2004, note = {To appear}, theme = {C}, workpackage = {2}, site = {genova}} @Article{AnconaLagorio04, author = "D. Ancona and G. Lagorio", title = "{S}tronger {T}ypings for {S}marter {R}ecompilation of {J}ava-like {L}anguages", journal = "Journal of Object Technology", volume = 3, number = 6, pages= "5--25", year = 2004, month = {June}, note = "Special issue: ECOOP 2003 workshop on Formal Techniques for Java-like Programs", theme = {E}, workpackage = {1}, site = {genova}} @InProceedings{AnconaZucca04, author = "D. Ancona and E. Zucca", title = "Principal Typings for {J}ava-like languages", booktitle=popl04, month = {January}, year=2004, publisher = acm, pages ={306--317}, theme = {E}, workpackage = {1}, site = {genova}} @InProceedings{AnconaEtAl04, author = {D. Ancona and S. Fagorzi and E. Zucca}, title = {A Calculus with Lazy Module Operators}, editor = {Jean-Jacques Levy and Ernst W. Mayr and John C. Mitchell}, pages={423--436}, publisher = kl, booktitle = {TCS 2004 (IFIP Int. Conf. on Theoretical Computer Science)}, year = {2004}, theme = {E}, workpackage = {2}, site = {genova}} @InProceedings{AnconaEtAl04a, author = {D. Ancona and S. Fagorzi and E. Zucca}, title = {A Calculus for Dynamic Reconfiguration with Low Priority Linking}, booktitle = {WOOD'04: Workshop on Object-Oriented Developments}, month ={August}, year = {2004}, theme = {E}, workpackage = {2}, site = {genova}} @InProceedings{FagorziEtAl04, author = {S. Fagorzi and E. Zucca and D. Ancona}, title = {Modeling Multiple Class Loaders by a Calculus for Dynamic Linking}, booktitle = oops04, publisher = acm, editor = {Hisham Haddad and Andrea Omicini and Roger L. Wainwright and Lorie M. Liebrock}, pages={1281--1288}, year = {2004}, month={March}, isbn = {1-58113-812-1}, theme = {E}, workpackage = {2}, site = {genova}} @Article{FagorziZucca04, author = "S. Fagorzi and E. Zucca", title = "A Case-Study in Encoding Configuration Languages: Multiple Class Loaders", journal = "Journal of Object Technology", year = 2004, note = {To appear}, theme = {A}, workpackage = {2}, site = {genova}} @Book{ronchi04book, Author = {Ronchi Della Rocca, Simona and Paolini, Luca}, Title = {The Parametric $\lambda$-Calculus: a Metamodel for Computation}, Publisher = "Springer-Verlag", Series = "Texts in Theoretical Computer Science: An EATCS Series", pages= 252, Address = "Berlin", year = 2004, url = {http://www.di.unito.it/~paolini/papers/PaoRdRlibro03.html}, year = 2004, theme = {BE}, workpackage = {2}, site = {genova}} @PhdThesis{paolini04phd, Author = {Paolini, Luca}, Title = {Lambda-theories: some investigations}, School = {Universit\`a di Genova and Universit\'e de la M\'editerran\'ee}, url = {http://www.di.unito.it/~paolini/papers/paolini03:PHDthesis.html}, year = 2003, theme = {BE}, workpackage = {2}, site = {genova}} @Article{paolini04iandc, Author = {Paolini, Luca and Ronchi Della Rocca, Simona}, Title = {Parametric parameter passing lambda-calculus}, Journal = {Information and Computation}, Volume = 189, Number = 1, Pages = {87-106}, url = {http://www.di.unito.it/~paolini/papers/paoRDR04:ppp.html}, year = 2004, theme = {E}, workpackage = {2}, site = {genova}} @InProceedings{paolini04itrs, author = {Paolini, Luca and Pimentel, Elaine and Ronchi Della Rocca, Simona}, title = "Lazy Strong Normalization", booktitle = {Proceedings of Workshops on Intersection Types and Related Systems {(ITRS'04)}}, year = 2004, series = {Electronic Notes in Theoretical Computer Science}, publisher = {Elsevier}, note = {A satellite workshops of the Joint Meeting ICALP2004/LICS2004.}, theme = {BE}, workpackage = {2}, site = {genova}} @InProceedings{paolini04cometa, author = {Paolini, Luca and Ronchi Della Rocca, Simona}, title = {Lazy logical semantics}, booktitle = {Proceedings of the Workshop of the {COMETA} Project on Computational Metamodels}, pages = {235-251}, year = 2004, editor = {Honsell, Furio and Lenisa, Marina and Miculan, Marino}, volume = {104C}, series = {Electronic Notes in Theoretical Computer Science}, abstract = {The lazy evaluation of the lambda-calculus, both in call-by-name and in call-by-value setting, is studied. Starting from a logical descriptions of two topological models of such calculi, a pre-order relation on terms, stratified by types, is defined, which grasps exactly the two operational semantics we want to model. Such a relation can be used for building two fully abstract models.}, publisher = {Elsevier}, documenturl = {http://www.di.unito.it/~paolini/papers/cometa5.pdf}, publisher = {Elsevier}, theme = {E}, workpackage = {2}, site = {genova}} @string{lncs = {Lecture Notes in Computer Science}} @string{springer = {Springer-Verlag}} @string{acm = {ACM Press}} @string{jfp = {Journal of Functional Programming}} @string{mscs = {Methematical Structures in Computer Science}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%% Les marroniers (reviennent tous les ans) %%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @Manual{0000-Ocaml-manual, theme = {AE}, workpackage = {1}, site = {inria}, title = {The {Objective} {Caml} system, documentation and user's manual -- release 3.08}, author = {Xavier Leroy and Damien Doligez and Jacques Garrigue and Didier Rémy and Jérôme Vouillon}, organization = {INRIA}, month = jul, year = 2004, url = {http://caml.inria.fr/ocaml/htmlman/} } %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 2004 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @InProceedings{2004-DiCosmo-Balat-Fiore, theme = {E}, workpackage = {1}, site = {inria}, author = {Vincent Balat and Di Cosmo, Roberto and Marcelo Fiore}, title = {Extensional Normalisation and Type-Directed Partial Evaluation for Typed Lambda Calculus with Sums}, booktitle = "31st ACM symposium on Principles of Programming Languages", YEAR = {2004}, month = jan, publisher = acm, pages = "64--76" } @InProceedings{2004-Frisch-Cardelli-icalp, theme = {EH}, workpackage = {1}, site = {inria}, author = {Alain Frisch and Luca Cardelli}, title = {Greedy regular expression matching}, booktitle = "31st International Colloquium on Automata, Languages and Programming", YEAR = {2004}, month = jul, publisher = springer, pages = "618-629" } @InProceedings{2004-Frisch-tcs, theme = {EH}, workpackage = {1}, site = {inria}, author = {Alain Frisch}, title = {Regular tree language recognition with static information}, booktitle = "3rd IFIP International Conference on Theoretical Computer Science", YEAR = {2004}, month = aug, publisher = "Kluwer Academic Publishers" } @InProceedings{2004-Frisch-Hosoya-Castagna-popl, author = {Haruo Hosoya and Alain Frisch and Giuseppe Castagna}, title = {Parametric Polymorphism for {XML}}, booktitle = "32nd ACM symposium on Principles of Programming Languages", YEAR = {2005}, month = jan, publisher = acm, note = {To appear}, theme = {EH}, workpackage = {1}, site = {inria} } @inproceedings{2004-Gauthier-Pottier, theme = {AE}, workpackage = {1}, site = {inria}, author = {Nadji Gauthier and François Pottier}, title = {Numbering Matters: First-Order Canonical Forms for Second-Order Recursive Types}, booktitle = {Proceedings of the 2004 {ACM} {SIGPLAN} International Conference on Functional Programming (ICFP'04)}, url ={http://cristal.inria.fr/~fpottier/publis/gauthier-fpottier-icfp04.pdf}, acm = {http://doi.acm.org/10.1145/1016850.1016872}, month = SEP, year = {2004}, pages = {150--161}, abstract = { We study a type system equipped with universal types and equirecursive types, which we refer to as $F_\mu$. We show that type equality may be decided in time $O(n\log n)$, an improvement over the previous known bound of $O(n^2)$. In fact, we show that two more general problems, namely entailment of type equations and type unification, may be decided in time $O(n\log n)$, a new result. To achieve this bound, we associate, with every $F_\mu$ type, a \emph{first-order canonical form}, which may be computed in time $O(n\log n)$. By exploiting this notion, we reduce all three problems to equality and unification of \emph{first-order} recursive terms, for which efficient algorithms are known.} } @inproceedings{2004-Hirschowitz-Leroy-Wells, theme = {AE}, workpackage = {1}, site = {inria}, author = {Tom Hirschowitz and Xavier Leroy and J. B. Wells}, title = {Call-by-Value Mixin Modules: Reduction Semantics, Side Effects, Types}, booktitle = {European Symposium on Programming}, volume = 2986, series = lncs, publisher = springer, pages = "64--78", year = {2004}, url = {http://cristal.inria.fr/~xleroy/publi/mixins-mm-esop2004.ps.gz}, abstract = {Mixin modules are a framework for modular programming that supports code parameterization, incremental programming via late binding and redefinitions, and cross-module recursion. In this paper, we develop a language of mixin modules that supports call-by-value evaluation, and formalize a reduction semantics and a sound type system for this language.} } @inproceedings{2004-Hirschowitz-Leroy-Wells-APPSEM, theme = {AE}, workpackage = {1}, site = {inria}, author = {Tom Hirschowitz and Xavier Leroy and J. B. Wells}, title = {Extended recursive definitions in call-by-value languages, with applications to mixin modules and recursive modules}, booktitle = {Electronic proceedings of the second APPSEM II Workshop}, city = {Tallin}, year = {2004}, month = apr } @InCollection{2004-Pottier-Remy-ATTAPL, theme = {AE}, workpackage = {1}, site = {inria}, author = "Fran{\c{c}}ois Pottier and Didier R{\'{e}}my", booktitle = "Advanced Topics in Types and Programming Languages", title = "The Essence of {ML} Type Inference", pages = "389--489", publisher = "MIT Press", year = "2005", editor = "Benjamin C. Pierce", chapter = "10", } @InProceedings{2004-Pottier-Gauthier-POPL, theme = {AE}, workpackage = {1}, site = {inria}, author = "François Pottier and Nadji Gauthier", title = "Polymorphic Typed Defunctionalization", booktitle = "31st ACM symposium on Principles of Programming Languages", publisher = acm, month = jan, year = "2004", pages = "89--98", url ="http://cristal.inria.fr/~fpottier/publis/fpottier-gauthier-popl04.pdf", abstract = {\emph{Defunctionalization} is a program transformation that aims to turn a higher-order functional program into a first-order one, that is, to eliminate the use of functions as first-class values. Its purpose is thus identical to that of \emph{closure conversion}. It differs from closure conversion, however, by storing a \emph{tag}, instead of a code pointer, within every closure. Defunctionalization has been used both as a reasoning tool and as a compilation technique. Defunctionalization is commonly defined and studied in the setting of a simply-typed $\lambda$-calculus, where it is shown that semantics and well-typedness are preserved. It has been observed that, in the setting of a polymorphic type system, such as ML or System F, defunctionalization is not type-preserving. In this paper, we show that extending System F with \emph{guarded algebraic data types} allows recovering type preservation. This result allows adding defunctionalization to the toolbox of type-preserving compiler writers.}, } @Unpublished{2004-Pottier-Regis-Gianas, theme = {ABE}, workpackage = {1}, site = {inria}, author = "François Pottier and Yann {Régis-Gianas}", title = "Towards efficient, typed {LR} parsers", url = "http://cristal.inria.fr/~fpottier/publis/fpottier-regis-gianas-jfp04.pdf", month = sep, year = "2004", abstract = {The LR parser generators that are bundled with many functional programming language implementations produce code that is unsafe, needlessly inefficient, or both. We show that, using generalized algebraic data types, it is possible to produce parsers that are well-typed (so they cannot unexpectedly crash or fail) and nevertheless efficient. This is a useful result as well as a nice exercise in programming with generalized algebraic data types.}, note = "Submitted to the \emph{Journal of Functional Programming}", } @PhdThesis{2004-Pottier-hdr, author = "François Pottier", title = "Types et contraintes", school = "Université Paris 7", month = dec, type = "Mémoire d'habilitation à diriger des recherches", year = "2004", url = "http://cristal.inria.fr/~fpottier/publis/fpottier-hdr.pdf" } @Unpublished{2004-Simonet-Pottier-hmg, author = "Vincent Simonet and François Pottier", title = "Constraint-Based Type Inference with Guarded Algebraic Data Types", note = "Submitted to \emph{ACM Transactions on Programming Languages and Systems}", month = jun, year = "2004", URL = "http://cristal.inria.fr/~fpottier/publis/simonet-pottier-hmg.pdf", } @PhdThesis{2004-Simonet-these, author = {Vincent Simonet}, TITLE = {Inférence de flots d'information pour {ML}: formalisation et implantation}, school = {Université Paris 7}, year = 2004, month = mar, URL = {http://cristal.inria.fr/~simonet/publis/simonet-these.pdf}, ABSTRACT = {This thesis describes the conception of an information flow analyser for a language of the ML family, from its theoretical foundation to the practical issues. The first part of the dissertation presents the tool that was implemented, Flow Caml, and illustrates its use on concrete example. The second part gives a formalization of the type system featured by Flow Caml, together with a proof of its correctness. This is the first type system for information flow analysis in a realistic programming language that has been formally proved. Lastly, the third part is devoted to the formalization and the proof of an efficient algorithm for type inference in the presence of structural subtyping and polymorphism. An instance of this algorithm is used to synthesize types in Flow Caml.} } @PhdThesis{2004-LeBotlan-these, author = {{Le Botlan}, Didier}, title = {{MLF}: Une extension de {ML} avec polymorphisme de second ordre et instanciation implicite.}, school = {École Polytechnique}, year = 2004, month = may, URL = "http://www.inria.fr/rrrt/tu-1071.html", abstract = { Nous nous intéressons à une extension de ML avec polymorphisme de première classe, à la manière du Système~{F}. Cette extension, nommée {MLF}, utilise les annotations de types d'ordre supérieur données explicitement dans le programme pour inférer de manière principale le type le plus général. Toute expression admet ainsi un type principal, qui dépend des annotations présentes initialement dans le programme. \par Toute expression de {ML} est typable dans {MLF} sans annotation supplémentaire. Les expressions du Système {F} sont encodées de manière systématique dans {MLF} en supprimant les abstractions et les applications de types, et en traduisant les annotations de types dans le langage de types de {MLF}. De plus, les paramètres de lambda-abstractions qui ne sont pas utilisés de manière polymorphe n'ont pas besoin d'être annotés. }} @InProceedings{2004-Yakobowski-LOPSTR, author = {J. B. Wells and Boris Yakobowski}, title = {Graph-Based Proof Counting and Enumeration with Applications for Program Fragment Synthesis}, pdf = {http://www.yakobowski.org/content/term-enumeration-final.pdf}, abstract = {For use in earlier approaches to automated module interface adaptation, we seek a restricted form of program synthesis. Given some typing assumptions and a desired result type, we wish to automatically build a number of program fragments of this chosen typing, using functions and values available in the given typing environment. We call this problem \emph{term enumeration}. To solve the problem, we use the Curry-Howard correspondence (propositions-as-types, proofs-as-programs) to transform it into a \emph{proof enumeration} problem for an intuitionistic logic calculus. We formally study proof enumeration and counting in this calculus. We prove that proof counting is solvable and give an algorithm to solve it. This in turn yields a proof enumeration algorithm.}, year = 2004, key = {LO{\relax PSTR} '04}, booktitle = {International Symposium on Logic-based Program Synthesis and Transformation 2004 (LOPSTR 2004)}, editor = {Sandro Etalle}, volume = {3049}, series = LNCS, publisher = Springer } % xaddress = {Verona, Italy}, @MastersThesis{2004-Yakobowski-DEA, author = {Boris Yakobowski}, title = {Étude sémantique d'un langage intermédiaire de type Static Single Assignment}, type = {{Master's} dissertation (mémoire de stage de {DEA})}, school = {ENS Cachan}, year = {2004}, month = sep, } %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%% INRIA SOPHIA %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @inproceedings{h04:fase, author = {M. Huisman and D. Gurov and C. Sprenger and G. Chugunov}, title = {Checking Absence of Illicit Applet Interactions: a Case Study}, booktitle = {Fundamental Approaches to Software Engineering, FASE 2004}, editor = {M. Wermelinger and T. Margaria}, pages = {84--98}, publisher = springer, series = LNCS, number = 2984, year = 2004, site = {inria}, workpackage = {1}, theme={D} } @techreport{h05:cats, title = "Factorising temporal specifications", author = "M. Huisman and K. Trentelman", INSTITUTION = {INRIA}, year = {2004}, number = {RR-5326}, note = "To appear in CATS 2005", site = {inria}, workpackage = {1}, theme={D} } @article{h:scp, title = {Formal Methods for Smart Cards: an experience report}, author = "C. Breunesse and N. Cataño and M. Huisman and B. Jacobs", note = "To appear", journal = "Science of Computer Programming", year = 2004, site = {inria}, workpackage = {1}, theme={D} } @InProceedings{h04:memocode, author = {C. Sprenger and D. Gurov and M. Huisman}, title = {Compositional Verification for Secure Loading of Smart Card Applets}, booktitle = {Second {ACM-IEEE} International Conference on Formal Methods and Models for Codesign ({MEMOCODE'04})}, pages = {211--222}, year = {2004}, editor = {C. Heitmeyer and J.-P. Talpin}, publisher = {{IEEE}}, site = {inria}, workpackage = {1}, theme={D} } @inproceedings{gpt04:csfw, author={G. Barthe, P. D'Argenio and T. Rezk}, title={{Secure Information Flow by Self-Composition}}, editor={R. Foccardi}, booktitle={Proceedings of CSFW'04}, pages={100-114}, publisher={IEEE Press}, year={2004}, site = {inria}, workpackage = {1}, theme={D} } @inproceedings{gt05:tldi, author={G. Barthe and T. Rezk}, title={Non-interference for a {JVM}-like language}, year={2005}, booktitle={Proceedings of {TLDI}'05}, editor={M. F\"ahndrich}, publisher={ACM Press}, note={To appear}, site = {inria}, workpackage = {1}, theme={E}} @inproceedings{m+04:cardis, author={M. Pavlova and G. Barthe and L. Burdy and M. Huisman and J.-L. Lanet}, title={Enforcing High-Level Security Properties For Applets}, editor={P. Paradinas and J.-J. Quisquater}, booktitle={{Proceedings of CARDIS'04}}, publisher={Kluwer}, year={2004}, pages={}, site = {inria}, workpackage = {1}, theme={D}} @inproceedings{gl04:fmse, author={G. Barthe and L. Prensa-Nieto}, title={Formally Verifying Information Flow Type Systems for Concurrent and Thread Systems}, booktitle={Proceedings of FMSE'04}, editor={M. Backes and D. Basin and M. Waidner}, publisher={ACM Press}, year={2004}, pages={13-22}, site = {inria}, workpackage = {1}, theme={E}} @inproceedings{gg04:fase, author ={G. Barthe and G. Dufay}, title = {{A Tool-Assisted Framework for Certified Bytecode Verification}}, year = {2004}, booktitle={Proceedings of {FASE}'04}, series=lncs, publisher=springer, volume= {2984}, pages= {99-113}, editors={M. Wermelinger and T. Margaria-Steffen}, site = {inria}, workpackage = {1}, theme= {D}} @inproceedings{gat04:vmcai, author={G. Barthe and A. Basu and T. Rezk}, title={Security Types Preserving Compilation}, year={2004}, booktitle={Proceedings of {VMCAI}'04}, series=lncs, publisher=springer, volume={2934}, editor="B. Steffen and G. Levi", pages={2--15}, site = {inria}, theme={E}} @article{gt04:jfp, author ={G. Barthe and T. Coquand}, title = {On the equational theory of non-normalizing Pure Type Systems}, journal= jfp, year = {2004}, volume=14, number=2, pages={191--209}, month=mar, theme={B}, workpackage = {1}, site = {inria}} @article{g+04:mscs, author = {G. Barthe and M. J. Frade and E. Giménez and L. Pinto and T. Uustalu}, title = {Type-Based Termination of Recursive Definitions}, year = {2004}, journal=mscs, month=feb, volume=14, issue=1, pages={97--141}, theme={B}, site = {inria}} @article{gl04:mscs, author = {G. Barthe}, title = {Type Isomorphisms and Back-and-Forth Coercions in Type Theory}, year = {2004}, journal=mscs, note={To appear}, theme={B}, workpackage = {1}, site = {inria}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%% INRIA RENNES %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @Article{Besson:05:Interfaces, author = "Fr\'ed\'eric Besson and Thomas de Grenier de Latour and Thomas Jensen", title = "Interfaces for stack inspection", journal = "Journal of Functional Programming", note = "To appear", year = {2005}, site = {inria}, workpackage = {1}, theme = {ACDE} } @InProceedings{CachJen:esop04, author = {David Cachera and Thomas Jensen and David Pichardie and Vlad Rusu}, title = {Extracting a data flow analyser in constructive logic}, booktitle = "Proc.~ESOP'04", series = "Springer LNCS", number = "2986", pages = "385 -- 400", year = "2004", note = "Extended version to appear in TCS", site = {inria}, theme = {BCD}, workpackage = {1} } @ARTICLE{BKKR-IJFCS-2001, AUTHOR = {Borovansk\'y, Peter and Kirchner, Claude and Kirchner, Helene and Ringeissen, Christophe}, TITLE = {Rewriting with strategies in {{\sf ELAN}}: a functional semantics}, JOURNAL = {{International Journal of Foundations of Computer Science}}, MONTH = {February}, NUMBER = {1}, PAGES = {69--98}, VOLUME = {12}, workpackage = {1}, site = {Loria}, theme = {BCD}, YEAR = {2001} } @ARTICLE{rhoCalIGLP-I+II-2001, AUTHOR = {Cirstea, Horatiu and Kirchner, Claude}, TITLE = {The rewriting calculus --- {Part~I {\em and} II}}, JOURNAL = {Logic Journal of the Interest Group in Pure and Applied Logics}, MONTH = {May}, NUMBER = {3}, PAGES = {427--498}, VOLUME = {9}, workpackage = {1}, site = {Loria}, theme = {BCDE}, YEAR = {2001} } @INPROCEEDINGS{cirstea02b, AUTHOR = {Cirstea, Horatiu and Kirchner, Claude and Liquori, Luigi and Wack, Benjamin}, TITLE = {{The rho cube \,: some results, some problems}}, BOOKTITLE = {{First International Workshop on Higher-Order Rewriting - HOR'02, Copenhague, Danemark}}, MONTH = {July}, ORGANIZATION = {D. Kesner, T. Nipkow \& F. van Raamsdonk}, YEAR = {2002}, workpackage = {1}, site = {Loria}, theme = {BE}, NOTE = {Held in conjunction with FLOC'02} } @INPROCEEDINGS{BarCirKirLiq-03, AUTHOR = {Barthe, G. and Cirstea, H. and Kirchner, C. and Liquori, L.}, TITLE = {{Pure Patterns Type Systems}}, BOOKTITLE = {Proc. of POPL}, MONTH = {January}, PAGES = {250--261}, PUBLISHER = {The ACM press}, workpackage = {1}, site = {Loria}, theme = {BCDE}, YEAR = {2003} } @INPROCEEDINGS{cirstea04c, AUTHOR = {Cirstea, Horatiu and Liquori, Luigi and Wack, Benjamin}, TITLE = {Rewriting Calculus with Fixpoints\,: Untyped and First-order Systems}, BOOKTITLE = {{Annual Workshop on the Types Working Group - TYPES'2003, Torino, Italie}}, EDITOR = {Stefano Berardi and Mario Coppo and Ferruccio Damiani}, MONTH = {Mar}, PAGES = {147-161}, PUBLISHER = {Springer}, SERIES = {Lecture Notes in Computer Science}, VOLUME = {3085}, workpackage = {1}, site = {Loria}, theme = {BE}, YEAR = {2004} } @INPROCEEDINGS{liquori04a, AUTHOR = {Liquori, Luigi and Wack, Benjamin}, TITLE = {The Polymorphic Rewriting Calculus\,: Type checking vs. Type inference}, BOOKTITLE = {{5th International Workshop on Rewriting Logic and its Applications - WRLA 2004, Barcelona, Spain}}, EDITOR = {Narciso Marti-Oliet and Manuel Clavel and Alberto Verdejo}, MONTH = {Mar}, ORGANIZATION = {Narciso Marti-Oliet}, PUBLISHER = {Elsevier}, SERIES = {Electronic Notes in Theoretical Computer Science}, workpackage = {1}, site = {Loria}, theme = {BE}, YEAR = {2004} } @INPROCEEDINGS{wack04a, AUTHOR = {Wack, Benjamin}, TITLE = {The Simply-typed Pure Pattern Type System Ensures Strong Normalization}, BOOKTITLE = {{3rd IFIP International Conference on Theoretical Computer Science - TCS'2004, Toulouse, France}}, EDITOR = {Jean-Jacques Lévy}, MONTH = {Aug}, ORGANIZATION = {Jean-Jacques Lévy}, PAGES = {633-646}, PUBLISHER = {{Kluwer} Academic Publishers}, workpackage = {1}, site = {Loria}, theme = {B}, YEAR = {2004} } @INPROCEEDINGS{cirstea04b, AUTHOR = {Cirstea, Horatiu and Faure, Germain and Kirchner, Claude}, TITLE = {A rho-calculus of explicit constraint application}, BOOKTITLE = {{5th International Workshop on Rewriting Logic and its Applications - WRLA'2004, Barcelona, Spain}}, EDITOR = {Narciso Marti-Oliet and Manuel Clavel and Alberto Verdejo}, MONTH = {Mar}, ORGANIZATION = {Narciso Marti-Oliet}, PUBLISHER = {Elsevier}, SERIES = {Electronic Notes in Theoretical Computer Science}, theme = {B}, YEAR = {2004} } %%%%%%%%%%%%%%%% @CONFERENCE{Gal03c, AUTHOR = {N. Biri and D. Galmiche}, TITLE = {A {S}eparation {L}ogic for {R}esource {D}istribution}, BOOKTITLE = {23rd Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS'03, LNCS 2914}, YEAR = {2003}, PAGES = {23-37}, MONTH = {December}, workpackage = {1}, site = {Loria}, theme = {D}, NOTE = {Mumbai, India} } @ARTICLE{Gal03a, AUTHOR = {D. Galmiche and D. M\'ery}, TITLE = {Semantic Labelled Tableaux for Propositional {BI} without bottom}, JOURNAL = {JLC}, YEAR = {2003}, VOLUME = {13}, NUMBER ={5}, PAGES = {707-753}, workpackage = {1}, site = {Loria}, theme = {D}, NOTE = {} } @CONFERENCE{Lar04a, AUTHOR = {D. Larchey-Wendling}, TITLE = {Counter-Model Search in {G}\"odel-{D}ummett logics}, BOOKTITLE = {2nd Int. Joint Conference IJCAR 2004, LNAI 3097}, YEAR = {2004}, PAGES = {274-288}, ADDRESS = {Cork, Ireland}, MONTH = {July}, workpackage = {1}, site = {Loria}, theme = {GH}, NOTE = {} } @CONFERENCE{Gal04c, AUTHOR = {D. Galmiche and D. M\'ery}, TITLE = {Resource Graphs and Countermodels in Resource Logics}, BOOKTITLE = {Int Workshop on Disproving: Non-theorems, Non-validity, Non-Provability}, YEAR = {2004}, PAGES = {59-75}, ADDRESS = {Cork, Ireland}, MONTH = {July}, workpackage = {1}, site = {Loria}, theme = {GH}, NOTE = {} } @CONFERENCE{Lar04b, AUTHOR = {D. Larchey-Wendling}, TITLE = {{G}\"odel-{D}ummett counter-models through matrix computation}, BOOKTITLE = {Int Workshop on Disproving: Non-theorems, Non-validity, Non-Provability}, YEAR = {2004}, PAGES = {77-87}, ADDRESS = {Cork, Ireland}, MONTH = {July}, workpackage = {1}, site = {Loria}, theme = {GH}, NOTE = {} } @PROCEEDINGS{Gal04d, TITLE = {Workshop on Logics for Resources, Processes and Programs, affiliated to ICALP - LICS 2004}, YEAR = {2004}, EDITOR = {D. Galmiche and P. O'Hearn and D. Pym}, ADDRESS = {Turku, Finland}, MONTH = {July}, workpackage = {1}, site = {Loria}, theme = {GH}, NOTE = {} } %%%%%%%%% Cansell - Theme D %%%%%%%% @INPROCEEDINGS{cansell04a, CRINNUMBER = {A04-R-091}, CATEGORY = {3}, EQUIPE = {MOSEL}, AUTHOR = {Cansell, Dominique and Culat, Jean-Fran\c{c}ois and Méry, Dominique and Proch, Cyril}, TITLE = {Derivation of SystemC code from abstract system models}, BOOKTITLE = {{Forum on specification \& Design Languages - FDL'04, Lille, France}}, YEAR ={ 2004}, MONTH ={ Sep}, workpackage = {1}, site = {Loria}, theme = {D}, KEYWORDS = {formal method, model, refinement, architecture}, } @TECHREPORT{proch04a, CRINNUMBER = {A04-R-237}, CATEGORY = {15}, EQUIPE = {MOSEL}, AUTHOR = {Proch, Cyril and Cansell, Dominique and Mery, Dominique}, TITLE = {Projet RNRT EQUAST \,; SP2 Spécification incrémentale du système}, YEAR ={ 2004}, TYPE = {Rapport de recherche}, MONTH ={ Oct}, INSTITUTION = {Loria}, workpackage = {1}, site = {Loria}, theme = {D}, KEYWORDS = {B event, model, refinement, proof}, } @INPROCEEDINGS{cansell04b, CRINNUMBER = {A04-R-328}, CATEGORY = {3}, EQUIPE = {MOSEL}, AUTHOR = {Cansell, Dominique and Méry, Dominique}, TITLE = {Tutorial on the event-based B method \,: Concepts and Case Studies}, BOOKTITLE = {{Logics of Formal Software Specification Languages - LFSL'2004, The High Tatras, Slovakia}}, YEAR ={ 2004}, EDITOR = {Dines Bjoerner and Martin Henson}, MONTH ={ Jun}, workpackage = {1}, site = {Loria}, theme = {D}, KEYWORDS = {B, specification, B event-based method}, } @INCOLLECTION{cansell04c, CRINNUMBER = {A04-R-416}, CATEGORY = {11}, EQUIPE = {MOSEL}, AUTHOR = {Cansell, Dominique and Hallerstede, Stefan and Oliver, Ian}, TITLE = {UML-B specification and hardware implementation of a Hamming coder/decoder}, BOOKTITLE = {{UML-B - Specification for Proven Embedded Systems Design}}, PUBLISHER = {{Kluwer} Academic Publishers }, YEAR ={ 2004}, EDITOR = {Jean Mermet}, CHAPTER = {16}, MONTH ={ Nov}, workpackage = {1}, site = {Loria}, theme = {D}, KEYWORDS = {UML, EventB, error correction}, } @ARTICLE{cansell04d, CRINNUMBER = {A04-R-417}, CATEGORY = {1}, EQUIPE = {MOSEL}, AUTHOR = {Cansell, Dominique and Hallerstede, Stefan and Zimmermann , Yann }, TITLE = {Construction sûre de systèmes électroniques}, JOURNAL = {Génie Logiciel }, YEAR ={ 2004}, VOLUME = {69 }, PAGES = {38-44 }, MONTH ={ Jun}, workpackage = {1}, site = {Loria}, theme = {D}, KEYWORDS = {B method, refinement, formal modelisation, proof}, } @INCOLLECTION{zimmermann04a, CRINNUMBER = {A04-R-441}, CATEGORY = {11}, EQUIPE = {MOSEL}, AUTHOR = {Zimmermann, Yann and Hallerstede, Stefan and Cansell, Dominique}, TITLE = {Formal modelling of electronic circuits using event-B, Case Study\,: SAE J1708 Serial Communication Link }, BOOKTITLE = {{UML-B - Specification for Proven Embedded Systems Design }}, PUBLISHER = {{Kluwer} Academic Publishers }, YEAR ={ 2004}, EDITOR = {Jean Mermet }, CHAPTER = {13}, MONTH ={ Nov}, workpackage = {1}, site = {Loria}, theme = {D}, KEYWORDS = { systems, refinement, formal modelling, proof}, } %%%%%%%%% Theme H et I %%%%%%%%%%%%% @INPROCEEDINGS{bournez04i, CRINNUMBER = {A04-R-419}, CATEGORY = {3}, EQUIPE = {PROTHEO}, AUTHOR = {Bournez, Olivier and Cucker, Felipe and Jacobé de Naurois, Paulin and Marion, Jean-Yves}, TITLE = {Tailoring Recursion to Characterize Non-Deterministic Complexity Classes Over Arbitrary Structures}, BOOKTITLE = {{2nd APPSEM II Workshop - APPSEM'2004, Tallinn, Estonia}}, YEAR ={ 2004}, MONTH ={ Apr}, URL = {http://www.loria.fr/publications/2004/A04-R-419/A04-R-419.ps}, KEYWORDS = {bss model, implicit complexity, complexity}, workpackage = {1}, site = {Loria}, theme={HI}, ABSTRACT = {We provide machine-independent characterizations of some complexity classes, over an arbitrary structure, in the model of computation proposed by L.Blum, M.Shub and S.Smale. We show that the levels of the polynomial hierarchy correspond to safe recursion with predicative minimization. The levels of the digital polynomial hierarchy correspond to safe recursion with digital predicative minimization. Also, we show that polynomial alternating time corresponds to safe recursion with predicative substitutions and that digital polynomial alternating time corresponds to safe recursion with digital predicative substitutions. }, } @INPROCEEDINGS{bonfante04b, CRINNUMBER = {A04-R-355}, CATEGORY = {3}, EQUIPE = {CALLIGRAMME}, AUTHOR = {Bonfante, Guillaume and Marion, Jean-Yves and Moyen, Jean-Yves}, TITLE = {On complexity analysis by quasi-interpretation}, BOOKTITLE = {{2nd Appsem II workshop - APPSEM'04, Tallinn, Estonia}}, YEAR ={ 2004}, PAGES = {85-95}, MONTH ={ Apr}, workpackage = {1}, site = {Loria}, theme={H}, KEYWORDS = {quasi-interprétation, termination, complexity, ressource}, ABSTRACT = {We present a survey on a method to analyse the program time and space complexity, based on termination orderings and quasi-interpretation. This method can be implemented to certify the runtime (or space) of programs. We demonstrate that the class of functions computed by first order functional programs over free algebras which terminate by permutation Path Ordering (resp. Lexicographic Path Ordering) and admit a quasi-interpretation bounded by a polynomial, is exactly the class of functions computable in polynomial time (resp. space).}, } @ARTICLE{marion04a, CRINNUMBER = {A04-R-348}, CATEGORY = {1}, EQUIPE = {CALLIGRAMME}, AUTHOR = {Marion, Jean-Yves}, TITLE = {Editorial \,: Implicit Computational Complexity (ICC)}, JOURNAL = {Theoretical Computer Science}, YEAR ={ 2004}, VOLUME = {318}, NUMBER = {1-2}, PAGES = {1}, MONTH ={ Jun}, workpackage = {1}, site = {Loria}, theme={H}, NOTE={Editeur scientifique invité}, KEYWORDS = {complexity, logic}, ABSTRACT = {This special issue is devoted to Implicit Computational Complexity (ICC), following the successful ICC workshop that took place in 2000 at Santa Barbara, CA, in affiliation with the 15th IEEE Symposium on Logic in Computer Science.}, } @ARTICLE{bournez04g, CRINNUMBER = {A04-R-285}, CATEGORY = {1}, EQUIPE = {PROTHEO}, AUTHOR = {Bournez, Olivier and Cucker, Felipe and Jacobé de Naurois, Paulin and Marion, Jean-Yves}, TITLE = {Implicit Complexity Over an Arbitrary Structure\,: Sequential and Parallel Polynomial Time}, JOURNAL = {Journal of Logic and Computation}, YEAR ={ 2004}, MONTH ={ Nov}, workpackage = {1}, site = {Loria}, theme={HI}, URL = {http://www.loria.fr/publications/2004/A04-R-285/A04-R-285.ps}, KEYWORDS = {blum shub smale model, implicit complexity, complexity}, ABSTRACT = {We provide several machine-independent characterizations of deterministic complexity classes in the model of computation proposed by L. Blum, M. Shub and S. Smale. We provide a characterization of partial recursive functions over any arbitrary structure. We show that polynomial time over an arbitrary structure can be characterized in terms of safe recursion. We show that polynomial parallel time over an arbitrary structure can be characterized in terms of safe recursion with substitutions. }, } @INPROCEEDINGS{bournez03b, CRINNUMBER = {A03-R-315}, CATEGORY = {3}, EQUIPE = {PROTHEO}, AUTHOR = {Bournez, Olivier and Cucker, Felipe and Jacobé de Naurois, Paulin and Marion, Jean-Yves}, TITLE = {Safe Recursion Over an Arbitrary Structure\,: PAR, PH and DPH}, BOOKTITLE = {{Fifth International Workshop on Implicit Computational Complexity - ICC'2003, Ottawa, Canada}}, YEAR ={ 2003}, VOLUME = {90}, SERIES = {Electronic Notes in Computer Science}, MONTH ={ Jun}, workpackage = {1}, site = {Loria}, theme={HI}, KEYWORDS = {complexity, blum shub smale model, safe recursion}, ABSTRACT = {Considering the Blum, Shub, and Smale computational model for real numbers, extended by Poizat to general structures, classical complexity can be considered as the restriction to finite structures of a more general notion of computability and complexity working over arbitrary structures. In a previous paper, we showed that the machine-independent characterization of Bellantoni and Cook of sequential polynomial time for classical complexity is actually the restriction to finite structures of a characterization of sequential polynomial time over arbitrary structures. In this paper, we prove that the same phenomenon happens for several other complexity classes\,: over arbitrary structures, parallel polynomial time corresponds to safe recursion with substitutions, and the polynomial hierarchy corresponds to safe recursion with predicative minimization. Our results yield machine-independent characterizations of several complexity classes subsuming previous ones when restricted to finite structures.}, } @INPROCEEDINGS{bournez03a, CRINNUMBER = {A03-R-314}, CATEGORY = {3}, EQUIPE = {PROTHEO}, AUTHOR = {Bournez, Olivier and Cucker, Felipe and Jacobé de Naurois, Paulin and Marion, Jean-Yves}, TITLE = {Computability over an Arbitrary Structure. Sequential and Parallel Polynomial Time}, BOOKTITLE = {{Foundations of Software Science and Computation Structures - FOSSACS'03, Warsaw, Poland}}, YEAR ={ 2003}, EDITOR = {Andrew D. Gordon}, VOLUME = {2620}, SERIES = {Lecture Notes in Computer Science}, PAGES = {185-199}, MONTH ={ Apr}, PUBLISHER = {Springer}, KEYWORDS = {complexity, blum shub smale model, safe recursion}, workpackage = {1}, site = {Loria}, theme = {HI}, ABSTRACT = {We provide several machine-independent characterizations of deterministic complexity classes in the model of computation proposed by L. Blum, M. Shub and S. Smale. We provide a characterization of partial recursive functions over any arbitrary structure. We show that polynomial time computable functions over any arbitrary structure can be characterized in term of safe recursive functions. We show that polynomial parallel time decision problems over any arbitrary structure can be characterized in terms of safe recursive functions with substitutions.}, } @INPROCEEDINGS{bournez04a, CRINNUMBER = {A04-R-287}, CATEGORY = {3}, EQUIPE = {PROTHEO}, AUTHOR = {Bournez, Olivier and Cucker, Felipe and Jacobé de Naurois, Paulin and Marion, Jean-Yves}, TITLE = {Tailoring Recursion to Characterize Non-Deterministic Complexity Classes Over Arbitrary Structures}, BOOKTITLE = {{3rd IFIP International Conference on Theoretical Computer Science - TCS'2004, Toulouse, France}}, YEAR ={ 2004}, MONTH ={ Aug}, PUBLISHER = {{Kluwer} Academic Press}, URL = {http://www.loria.fr/publications/2004/A04-R-287/A04-R-287.ps}, KEYWORDS = {bss model, implicit complexity, complexity}, workpackage = {1}, site = {Loria}, theme = {HI}, ABSTRACT = {We provide machine-independent characterizations of some complexity classes, over an arbitrary structure, in the model of computation proposed by L.Blum, M.Shub and S.Smale. We show that the levels of the polynomial hierarchy correspond to safe recursion with predicative minimization. The levels of the digital polynomial hierarchy correspond to safe recursion with digital predicative minimization. Also, we show that polynomial alternating time corresponds to safe recursion with predicative substitutions and that digital polynomial alternating time corresponds to safe recursion with digital predicative substitutions. }, } %THEME A @Misc{LS-04b, author = {L. Liquori and A.Spiwack}, title = {{Inferring Types for Functional Methods}}, howpublished = {Manuscript}, year = {2004}, workpackage = {1}, site = {Loria}, theme={A}, note = {\url{http://www.sop-inria.fr/mirho/Luigi.Liquori/PAPERS/t41.ps.gz}} } @Misc{LS-04a, author = {L. Liquori and A.Spiwack}, title = {{Featherweight-Trait Java, A Trait-based Extension for FJ}}, howpublished = {Manuscript}, year = {2004}, workpackage = {1}, site = {Loria}, theme={A}, note = {\url{http://www.sop-inria.fr/mirho/Luigi.Liquori/PAPERS/ftj.ps.gz}} } @Misc{FL-04, author = {S. Fechter and L. Liquori}, title = {{Mini-Foc: A Kernel Calculus for Certified Computer Algebra [Ongoing Work]}}, howpublished = {Manuscript}, year = {2004}, workpackage = {1}, site = {Loria}, theme={A}, note = {\url{http://www.sop-inria.fr/mirho/Luigi.Liquori/PAPERS/minifoc.ps.gz}} } @Article{CLM-04, author = {A. Ciaffaglione and L. Liquori and M. Miculan}, title = {{Reasoning about Calculi of Objects in (Co)Inductive Type Theories with the Theory of Contexts}}, journal = {Journal of Automated Reasoning}, year = {200X}, publisher = {Kluwer}, workpackage = {1}, site = {Loria}, volume = {}, number = {}, theme={A}, note = {Under Major Revision, \url{http://www.sop-inria.fr/mirho/Luigi.Liquori/PAPERS/jar-04.ps.gz}} } @InProceedings{DLLL-04, author = {D. Dougherty and P. Lescanne and L. Liquori and F. Lang}, title = {{Addressed Term Rewriting Systems: Syntax, Semantics, and Pragmatics [Extended Abstract]}}, booktitle = {Proc. of TERMGRAPH, International Workshop on Term Graph Rewriting}, year = {2004}, series = {ENTCS}, publisher = {Elsevier}, number = {To appear}, workpackage = {1}, site = {Loria}, theme={A}, note = { \url{http://www.sop-inria.fr/mirho/Luigi.Liquori/PAPERS/termgraph-04.ps.gz}} } %THEME B @Misc{L-04b, author = {L. Liquori}, title = {{Intersection Types {\em \`a la} Church}}, howpublished = {Manuscript}, year = {2004}, workpackage = {1}, site = {Loria}, theme={B}, note = {\url{http://www.sop-inria.fr/mirho/Luigi.Liquori/PAPERS/inter.ps.gz}} } @Misc{L-04a, author = {L. Liquori}, title = {{iRho: the Software [System Description]}}, howpublished = {Manuscript}, year = {2004}, workpackage = {1}, site = {Loria}, theme={B}, note = {\url{http://www.sop-inria.fr/mirho/Luigi.Liquori/PAPERS/iRhoSW.ps.gz}} } @Misc{LS-04c, author = {L. Liquori and A.Spiwack}, title = {{An Object-Oriented Logical Framework [Preliminary Report]}}, howpublished = {Manuscript}, year = {2004}, workpackage = {1}, site = {Loria}, theme={B}, note = {\url{http://www.sop-inria.fr/mirho/Luigi.Liquori/PAPERS/d41.ps.gz}} } @InProceedings{CW-04, author = {L. Liquori and B. Wack}, title = {{The Polymorphic Rewriting-calculus [Type Checking {\em v.s.} Type Inference]}}, booktitle = {Proc. of WRLA, International Workshop on Rewriting Logic and its Applications}, year = {2004}, series = {ENTCS}, publisher = {Elsevier}, workpackage = {1}, site = {Loria}, number = {}, theme={B}, note = { \url{http://www.sop-inria.fr/mirho/Luigi.Liquori/PAPERS/wrla-04.ps.gz}} } @InProceedings{LR-04, author = {L. Liquori and S. Ronchi della Rocca}, title = {{Towards and Intersection Typed System {\em \`a la} Church}}, booktitle = {Proc. of ITRS, Workshop on Intersection Types and Related Systems}, year = {2004}, series = {ENTCS}, publisher = {Elsevier}, number = {To appear}, workpackage = {1}, site = {Loria}, theme={B}, note = { \url{http://www.sop-inria.fr/mirho/Luigi.Liquori/PAPERS/itrs-04.ps.gz}} } @InProceedings{LS-04, author = {L. Liquori and B.P. Serpette}, title = {{iRho: an Imperative Rewriting Calculus}}, booktitle = {Proc. of PPDP, ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming}, pages = {167-178}, year = {2003}, publisher = {ACM}, workpackage = {1}, site = {Loria}, theme={B}, note = {(47 \%) \url{http://www.sop-inria.fr/mirho/Luigi.Liquori/PAPERS/popl-03.ps.gz}} } %%%%%%%% @INPROCEEDINGS{bournez04d, CRINNUMBER = {A04-R-291}, CATEGORY = {3}, EQUIPE = {PROTHEO}, AUTHOR = {Bournez, Olivier and Hainry, Emmanuel}, TITLE = {An analog Characterization of Elementarily Computable Functions Over the Real Numbers}, BOOKTITLE = {{31st International Colloqiuim on Automata, Languages and Programming - ICALP'2004, Turku, Finland}}, YEAR ={ 2004}, EDITOR = {Diaz, Josep and KarhumŠki, Juhani and Lepisto, Arto and Sannella, Donald Theodore}, VOLUME = {3142}, SERIES = {Lecture Notes in Computer Science}, PAGES = {269-280}, MONTH ={ Jul}, workpackage = {1}, site = {Loria}, theme={HI}, PUBLISHER = {Springer}, KEYWORDS = {analog models, complexity, computability}, ABSTRACT = {We present an analog and machine-independent algebraic characterizations of elementarily computable functions over the real numbers in the sense of recursive analysis\,: we prove that they correspond to the smallest class of functions that contains some basic functions, and closed by composition, linear integration, and a simple limit schema. We generalize this result to all higher levels of the Grzegorczyk Hierarchy. Concerning recursive analysis, our results provide machine-independent characterizations of natural classes of computable functions over the real numbers, allowing to define these classes without usual considerations on higher-order (type 2) Turing machines. Concerning analog models, our results provide a characterization of the power of a natural class of analog models over the real numbers.}, } @INPROCEEDINGS{bournez04c, CRINNUMBER = {A04-R-290}, CATEGORY = {3}, EQUIPE = {PROTHEO}, AUTHOR = {Bournez, Olivier and Hainry, Emmanuel}, TITLE = {Real Recursive Functions and Real Extensions of Recursive Functions}, BOOKTITLE = {{Machines and Universal Computations - MCU'2004, Saint-Petersburg, Russia}}, YEAR ={ 2004}, MONTH ={ Sep}, workpackage = {1}, site = {Loria}, theme={HI}, KEYWORDS = {analog models, complexity, computability}, ABSTRACT = {Recently, functions over the reals that extend elementarily computable functions over the integers have been proved to correspond to the smallest class of real functions containing some basic functions and closed by composition and linear integration. We extend this result to all computable functions\,: functions over the reals that extend total recursive functions over the integers are proved to correspond to the smallest class of real functions containing some basic functions and closed by composition, linear integration and a very natural unique minimization schema.}, } @INPROCEEDINGS{bournez04b, CRINNUMBER = {A04-R-289}, CATEGORY = {3}, EQUIPE = {PROTHEO}, AUTHOR = {Bournez, Olivier and Hainry, Emmanuel}, TITLE = {An analog Characterization of Elementarily Computable Functions Over the Real Numbers}, BOOKTITLE = {{2nd APPSEM II Workshop - APPSEM'2004, Tallinn, Estonia}}, YEAR ={ 2004}, MONTH ={ Apr}, workpackage = {1}, site = {Loria}, theme={HI}, URL = {http://www.loria.fr/publications/2004/A04-R-289/A04-R-289.ps}, KEYWORDS = {analog models, complexity, computability}, ABSTRACT = {We present an analog and machine-independent algebraic characterizations of elementarily computable functions over the real numbers in the sense of recursive analysis\,: we prove that they correspond to the smallest class of functions that contains some basic functions, and closed by composition, linear integration, and a simple limit schema. We generalize this result to all higher levels of the Grzegorczyk Hierarchy. Concerning recursive analysis, our results provide machine-independent characterizations of natural classes of computable functions over the real numbers, allowing to define these classes without usual considerations on higher-order (type 2) Turing machines. Concerning analog models, our results provide a characterization of the power of a natural class of analog models over the real numbers.}, } @inproceedings{Dennis:disproving04, theme = {B}, site = {nottingham}, author= "Louise Dennis", title = "{The Use of Proof Planning Critics to Diagnose Errors in the Base Cases of Recursive Programs}", year = "2004", editor = "W. Ahrendt and P. Baumgartner and H. de Nivelle", pages = "47--58", booktitle = "IJCAR 2004 Workshop on Disproving: Non-Theorems, Non-Validity, Non-Provability" } @inproceedings{alti:flops04, theme = {BE}, site = {nottingham}, author = {Thorsten Altenkirch and Tarmo Uustalu}, title = {{Normalization by Evaluation for $\lambda^{\to 2}$}}, booktitle = {Functional and Logic Programming}, isbn = {3-540-21402-X}, year = {2004}, number = {2998}, series = {LNCS}, pages = {260 - 275}, } @unpublished{alti:qml-draft, theme = {BE}, site = {nottingham}, author = {Thorsten Altenkirch and Jonathan Grattage}, title = {{A Functional Quantum Programming Language}}, note = {Submitted for publication, available as quant-ph/0409065}, month = {July}, year = {2004}, } @inproceedings{hutton-mpc04, theme = {BD}, site = {nottingham}, author = "Graham Hutton and Joel Wright", title = "{Compiling Exceptions Correctly}", booktitle = "{Proceedings of the 7th International Conference on Mathematics of Program Construction}", address = "Stirling, Scotland", series = "Lecture Notes in Computer Science", volume = 3125, publisher = "Springer", month = jul, year = 2004 } @unpublished{hutton-tfp04, theme = {BDF}, site = {nottingham}, author = "Graham Hutton and Joel Wright", title = "{Calculating an Exceptional Machine}", note = "Submitted to the Symposium on Trends in Functional Programming", year = 2004 } @unpublished{hutton-fi04, theme = {BD}, site = {nottingham}, author = "Jeremy Gibbons and Graham Hutton", title = "{Proof Methods for Corecursive Programs}", note = "Submitted to Fundamenta Informaticae Special Issue on Program Transformation", month = mar, year = 2004 } @unpublished{hutton-book, theme = {B}, site = {nottingham}, author = "Graham Hutton", title = "{Programming in Haskell}", note = "In preparation", year = 2004 } @inproceedings{atannasow:jeuring:mpc04, theme = {BE}, site = {utrecht}, author = {Frank Atanassow and Johan Jeuring}, title = {{Inferring Type Isomorphisms Generically}}, year = 2004, booktitle = {{Proceedings of the 7th International Conference on Mathematics of Program Construction, MPC'04}}, editor = {Dexter Kozen}, series = "LNCS", volume = "3125", publisher = "Springer-Verlag", pages = "32--53" } @inproceedings{atannasow:clarke:jeuring:padl04, theme = {BEH}, site = {utrecht}, author = {Frank Atanassow and Dave Clarke and Johan Jeuring}, title = {{{UUXML}: A Type-Preserving {XML S}chema-{H}askell Data Binding}}, year = 2004, booktitle = {{Proceedings 6th International Symposium on Practical Aspects of Declarative Languages, PADL'04}}, editor = {Bharat Jayaraman}, series = "LNCS", volume = "3057", publisher = "Springer-Verlag", pages = "71--85" } @article{tidatascp, theme = {BE}, site = {utrecht,bonn}, author = {Ralf Hinze and Johan Jeuring and Andres L\"oh}, title = {{Type-Indexed Data Types}}, journal = "Science of Computer Programming", year = 2004, volume = "51", number = "1-2", pages = "117-151" } @phdthesis{loh-thesis, theme = {BE}, site = {utrecht}, author = {Andres L\"oh}, title = {{Exploring Generic Haskell}}, school = {Utrecht University}, year = 2004 } @inproceedings{ambler-crole-momigiliano, theme = {BD}, site = {leicester}, author = "Simon Ambler and Roy Crole and Alberto Momigliano", title = "{A Combinator and Presheaf Topos Model for Primitive Recursion over Higher Order Abstract Syntax}", booktitle = "{Collegium Logicum, Proceedings of the Kurt Godel Society}", pages = "83--89", publisher = "Springer-Verlag", year = 2004 } @inproceedings{ghani-icalp04, theme = {B}, site = {leicester}, author = {Michael Abbott and Thorsten Altenkirch and Neil Ghani}, title = {{Representing Nested Inductive Types using W-types}}, year = {2004}, booktitle = {Proceedings of International Colloquium on Automata, Languages and Programming, ICALP 2004}, volume = {3142}, pages = {59-71}, series = {Lecture Notes in Computer Science}, publisher = {Springer Verlag} } @inproceedings{ghani-mpc04, theme = {B}, site = {leicester}, author = {Michael Abbott and Thorsten Altenkirch and Neil Ghani and Conor McBride}, title = {{Constructing Programs with Quotient Types}}, booktitle = {Procedings of Mathematics of Program Construction 2004}, pages = {2-15}, year = {2004}, number = {3125}, series = {Lecture Notes in Computer Science}, publisher = {Springer Verlag} } @unpublished{ghani-cmcs04, theme = {G}, site = {leicester}, author = {Neil Ghani and Bjorn Victor and Kidane Yemane}, title = {{Relationally Staged Computation in the $\pi$-calculus}}, note = {To appear, Proceedings of CMCS 2004}, } @inproceedings{ghani-aplas04, theme = {B}, site = {leicester}, author = {Neil Ghani and Tarmo Uustalu and Varmo Vene}, title = {{Build, Augment, Destroy. Universally}}, year = {2004}, booktitle = {Proceedings of Programming Languages and Systems: Second Asian Symposium, APLAS, 2004}, volume = {3302}, pages = {327-341}, series = {Lecture Notes in Computer Science}, publisher = {Springer Verlag} } @inproceedings{ghani-wood04, theme = {A}, site = {leicester}, author = {Neil Ghani and Johan Glimming}, title = {{Difunctorial Semantics of Object Calculus}}, booktitle = {Electronic Notes in Theoretical Computer Science}, volume = {To Appear}, issue = {}, publisher = {Elsevier Science Publishers}, editor = {}, year = {2004} } @article{ghani-tia04, theme = {C}, site = {leicester}, author = {Neil Ghani and Tarmo Uustalu}, title = {{Coproducts of Ideal Monads}}, journal = {Journal of Theoretical Informatics and Applications}, number = {38}, pages = {321-342}, year = {2004} } @Unpublished{AehligMirandaOng04, author = {Aehlig, Klaus and Miranda, Jolie G. de and Ong, C.-H. Luke}, title = {The Monadic Second Order Theory of Trees Given by Arbitrary Level-Two Recursion Schemes Is Decidable}, note = {Submitted to TLCA2005} } @Unpublished{AehligMirandaOng04a, author = {Aehlig, Klaus and Miranda, Jolie G. de and Ong, C.-H. Luke}, title = {Safety is Not a Restriction at Level Two for String Languages}, note = {Submitted for publication} } @techreport{AehligMirandaOng04ax, author = {Aehlig, Klaus and Miranda, Jolie G. de and Ong, C. H. Luke}, title = {Safety is not a restriction at level 2 for string languages}, institution={Oxford University Computing Laboratory}, type={Technical Report}, number={PRG-RR-04-23}, note={Extended abstract submitted to FOSSACS2005}, year = {2004}} @InProceedings{ Gibbons2004:Metamorphisms, author="Jeremy Gibbons", title="Streaming Representation-Changers", booktitle="Mathematics of Program Construction", volume="3125", pages="142-168", url="http://www.springerlink.com/index/LHQ73WU5GU686976", series="Lecture Notes in Computer Science", editor="Dexter Kozen", year="2004", month=jul, abstract="\emph{Unfolds} generate data structures, and \emph{folds} consume them. A \emph{hylomorphism} is a fold after an unfold, generating then consuming a \emph{virtual data structure}. A \emph{metamorphism} is the opposite composition, an unfold after a fold; typically, it will convert from one data representation to another. In general, metamorphisms are less interesting than hylomorphisms: there is no automatic \emph{fusion} to \emph{deforest} the intermediate virtual data structure. However, under certain conditions fusion is possible: some of the work of the unfold can be done before all of the work of the fold is complete. This permits \emph{streaming metamorphisms}, and among other things allows conversion of \emph{infinite data representations}. We present the theory of metamorphisms and outline some examples." } @Unpublished{ Gibbons2004:Spigot, author="Jeremy Gibbons", title="Unbounded Spigot Algorithms for the Digits of $\pi$", note="Submitted for publication", year="2004", month=aug, abstract="Rabinowitz and Wagon (\textit{American Mathematical Monthly} 102(3):195--203, 1995) present a \emph{spigot algorithm} for computing the digits of $\pi$. A spigot algorithm yields its outputs incrementally, and does not reuse them after producing them. Their algorithm is inherently \emph{bounded}; it requires a commitment in advance to the number of digits to be computed, and in fact might still produce an incorrect last few digits. We propose some \emph{streaming algorithms} based on the same and similar characterizations of $\pi$, with the same incremental characteristics but without requiring the prior bound." } @Unpublished{ Gibbons*2004:Enumerating, author="Jeremy Gibbons and David Lester and Richard Bird", title="Enumerating the Rationals", note="Submitted for publication", year="2004", month=aug, annote="" } @article{ Martin*2004:Disciplined, author="Clare Martin and Jeremy Gibbons and Ian Bayley", title="Disciplined, Efficient, Generalised Folds for Nested Datatypes", journal="Formal Aspects of Computing", year="2004", volume="16", number="1", pages="19-35", abstract="Nested (or non-uniform, or non-regular) datatypes have recursive definitions in which the type parameter changes. Their folds are restricted in power due to type constraints. Bird and Paterson introduced \emph{generalised folds} for extra power, but at the cost of a loss of efficiency: folds may take more than linear time to evaluate. Hinze introduced \emph{efficient generalised folds} to counter this inefficiency, but did so in a pragmatic way, at the cost of a loss of reasoning power: without categorical or equivalent underpinnings, there are no universal properties for manipulating folds. We combine the efficiency of Hinze's construction with the powerful reasoning tools of Bird and Paterson's." } @MastersThesis{ Oliveira2004:Datatype, author="Bruno Cesar dos Santos Oliviera", title="Datatype-Generic Programming: A Functional Exploration", school="Oxford University Computing Laboratory", year="2004", month=oct, type="Transfer of status dissertation", annote="" } @inproceedings{AGMOS04, author={S. Abramsky and D. R. Ghica and A. S. Murawski and C.-H. L. Ong and I. D. B. Stark}, title={Nominal Games and Full Abstraction for the Nu-Calculus}, booktitle={Proceedings of LICS}, publisher={IEEE Computer Society Press}, pages={150--159}, year=2004} @incollection{GMO04, author={D. R. Ghica and A. S. Murawski and C.-H. L. Ong}, title={Syntactic Control of Concurrency}, booktitle={Proceedings of ICALP}, publisher={Springer-Verlag}, pages={683--694}, note={Lecture Notes in Computer Science Vol. 3142}, year=2004} @article{GMO04b, author={D. R. Ghica and A. S. Murawski and C.-H. L. Ong}, title={Syntactic Control of Concurrency}, journal={Theoretical Computer Science}, note={special ICALP'04 issue, accepted for publication},year={to appear}} @article{Mur04b, author={A. S. Murawski}, title={Games for complexity second-order call-by-name programs}, journal={Theoretical Computer Science}, note={special issue: Game Theory meets Computer Science, accepted for publication},year={to appear}} @unpublished{Mur04, author={A. S. Murawski}, title={Functions with local state: regularity and undecidability}, note={submitted for publication, 41pp.}} @InProceedings{Ghica04, author = {Dan R. Ghica}, title = {Semantical Analysis of Noninterference 3, An Operational Approach}, booktitle = {European Symposium on Programming (ESOP)}, year = {2004}, volume = {2986}, series = {LNCS}, address = {Barcelona, Spain}, } @InProceedings{GhicaMurawski04, author = {D. R. Ghica and A. S. Murawski}, title = {Angelic Semantics of Fine-Grained Concurrency}, booktitle = {Foundations of Software Science and Computation Structures}, year = {2004}, series = {LNCS}, address = {Barcelona}, month = {April}, publisher = {Springer}, } @InProceedings{AGMO04, author = {S. Abramsky and D. R. Ghica and A. S. Murawski and C.-H. L. Ong}, title = {Applying Game Semantics to Compositional Software Modeling and Verification}, booktitle = {Tenth International Conference on Tools and Algorithms for the Construction and Analysis of System}, year = {2004}, series = {LNCS}, address = {Barcelona}, month = {April}, publisher = {Springer}, } @Incollection{Coecke:Logic, author= "Coecke, B. and Moore, D. J. and Smets, S.", title= "Logic of Dynamics \& Dynamics of Logic: Some Paradigm Examples", booktitle= "Logic, Epistemology and the Unity of Science", pages = "111-196", editor = "D.M. Gabbay and S. Rahman and J.P. Van Bendegem", year = "2004", publisher = "Kluwer", note = "(Invited) Available at arXiv:math.LO/0106059", } @Inproceedings{Baltag:Algebra, author = "Baltag, A. and Coecke, B. and Sadrzadeh, M.", title = "Algebra and Sequent Calculus for Epistemic Actions", booktitle = "Proceedings of the Logic and Communication in Multi-Agent Systems workshop at the 16th European Summer School in Logic, Language and Information", series = "Electronic Notes in Theoretical Computer Science", publisher = "Elsevier", year = "2004", note = "Available at arXiv:quant-ph/0402130", } @Inproceedings{Baltag:Epistemic, author = "Baltag, A. and Coecke, B. and Sadrzadeh, M.", title = "Epistemic Actions as Resources", booktitle = "Proceedings of the Logics for Resources, Processes and Programs workshop at the 19th annual IEEE Symposium on Logic in Computer Science", publisher = "Journal of Logic and Computation (post proceedings)", year = "2004", } @Inproceedings{AC1, author = "Abramsky, S. and Coecke, B.", title = "A Categorical Semantics of Quantum Protocols", booktitle = "Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LiCS)", publisher = "IEEE Computer Science Press", year = "2004", note = "Available at arXiv:quant-ph/0402130", } @Unpublished{AC2, author = "Abramsky, S. and Coecke, B.", title = "Abstract Physical Traces", year = "2004", note = "Theory and Applications of Categories. (Invited Paper)", } @Unpublished{Coe1, author = "Coecke, B.", title = "The Logic of Entanglement", year = "2004", note = "Submitted to Physical Review A. Available at arXiv:quant-ph/0402014",} @Inproceedings{Coe2, author = "Coecke, B.", title = "Quantum Information Flow, Concretely, Abstractly", booktitle = "Proceedings of the 2nd International Workshop on Quantum Programming Languages", editor = "P. Selinger", publisher = "TUCS General Publication", year = "2004", } @Inproceedings{Coe4, author = "Coecke, B.", title = "Entropic Geometry from Logic", booktitle = "Proceedings Mathematical Foundations for Programming Semantics 2004", series = "Electronic Notes in Theoretical Computer Science", publisher = "Elsevier", year = "2004", note = "Available at arXiv:quant-ph/0212065", } @Inproceedings{Coe3, author = "Coecke, B.", title = "Quantum Information Flow, Concretely, and Axiomatically", booktitle = "Proceedings of Quantum Informatics 2004", publisher = "SPIE Press (SPIE:=The International Society for Optical Engineering)", year = "2004", note = "(Invited Paper)", } @Inproceedings{CM, author = "Coecke, B. and Martin, K.", title = "Partiality in Physics.", booktitle = "In Quantum Theory: Reconsideration of the Foundations II", publisher = "World Scientific", editor = "A. Khrennikov", year = "2004", note = "(Invited Paper) Available at arXiv:quant-ph/0312044", } @Article{CS, author = "Coecke, B. and von Smets, S.", title = "The {S}asaki-Hook is not a [Static] Implicative Connective but Induces a Backward [in Time] Dynamic One that Assigns Causes", journal = "International Journal of Theoretical Physics", year = "2004", volume = "43", pages = "131-169", } @Article{Baltag-Moss, author = "Baltag, A. and Moss, L.~S.", title = "Logics for Epistemic Programs", journal = "Synthese", year = "2004", volume = "139", pages = "165-224", } @unpublished{abc, author = "abc", title = "The {A}spect{B}ench {C}ompiler", note = "Release 1.0.0, October 22, 2004", url = "http://aspectbench.org"} @inproceedings{964004, author = {Ganesh Sittampalam and Oege de Moor and Ken Friis Larsen}, title = {Incremental execution of transformation specifications}, booktitle = {Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, year = {2004}, isbn = {1-58113-729-X}, pages = {26--38}, location = {Venice, Italy}, doi = {http://doi.acm.org/10.1145/964001.964004}, publisher = {ACM Press}, } @inproceedings{1028990, author = {Bruno Dufour and Christopher Goard and Laurie Hendren and Oege de Moor and Ganesh Sittampalam and Clark Verbrugge}, title = {Measuring the dynamic behaviour of {AspectJ} programs}, booktitle = {Proceedings of the 19th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications}, year = {2004}, isbn = {1-58113-831-9}, pages = {150--169}, location = {Vancouver, BC, Canada}, doi = {http://doi.acm.org/10.1145/1028976.1028990}, publisher = {ACM Press}, } @inproceedings{976283, author = {Ran Ettinger and Mathieu Verbaere}, title = {Untangling: a slice extraction refactoring}, booktitle = {Proceedings of the 3rd International Conference on Aspect-Oriented Software Development}, year = {2004}, isbn = {1-58113-842-3}, pages = {93--101}, location = {Lancaster, UK}, doi = {http://doi.acm.org/10.1145/976270.976283}, publisher = {ACM Press}, } @techreport{cc05abc, author = "Pavel Avgustinov and Aske Simon Christensen and Laurie Hendren and Sascha Kuzins and Jennifer Lhot{\'{a}}k and Ondrej Lhot{\'{a}}k and Oege de Moor and Damien Sereni and Ganesh Sittampalam and Julian Tibble", title = "Building the {\em abc} {AspectJ} compiler with {P}olyglot and {S}oot", institution = "aspectbench.org", number = "abc-2004-2", year = "2004", note = "Submitted to CC 2005"} @techreport{pldi05abc, author = "Pavel Avgustinov and Aske Simon Christensen and Laurie Hendren and Sascha Kuzins and Jennifer Lhot{\'{a}}k and Ondrej Lhot{\'{a}}k and Oege de Moor and Damien Sereni and Ganesh Sittampalam and Julian Tibble", title = "Optimising {AspectJ}", institution = "aspectbench.org", number = "abc-2004-3", year = "2004", note = "Submitted to PLDI 2005"} @phdthesis{hunke04, author = "Yorck Huenke", title = "Semantics of a lazy dependently typed programming language", school = "University of Oxford", year = "2004"} @techreport{sereni04, author = "Damien Sereni", title = "Size-change termination of higher-order functional programs", institution = "Oxford University Computing Laboratory", series = "Programming Research Group Technical reports", number = "RR-04-20", year = "2004"} @techreport{lynagh04, author = "Ian Lynagh", title = "Typing {T}emplate {H}askell: Soft Types", institution = "Oxford University Computing Laboratory", series = "Programming Research Group Technical reports", number = "RR-04-19", year = "2004"} @UNPUBLISHED{KL04, AUTHOR = {Delia Kesner and St\'ephane Lengrand}, TITLE = {An Explicit Operator Calculus as the Syntactic Counterpart to a Proof-Net Model}, NOTE = {Available at \url{http://www.pps.jussieu.fr/~kesner/papers}}, YEAR = 2004 } @unpublished{L04, AUTHOR = {Benjamin Leperchey}, TITLE = {Times and Games}, YEAR = {2004}, note = {Submitted}, DMI-CATEGORY = {subm} } @Article{Baillot04, author = {Baillot, P.}, title = {Type inference for Light affine logic via constraints on words}, journal = {Theoretical Computer Science}, year = {2004}, note = {35 pages, to appear}, } @InProceedings{BaillotTerui04, author = {Baillot, P. and Terui, K.}, title = {Light types for polynomial time computation in lambda-calculus}, booktitle = {Proceedings of the annual Symposium on Logic in Computer Science (LICS'04)}, pages = {266--275}, address={Turku, Finland}, month={July}, year = {2004}, organization = {IEEE}, publisher = {IEEE Computer Press} } @InProceedings{BaillotMogbil04, author = {Baillot, P. and Mogbil, V.}, title = {Soft lambda-calculus: a language for polynomial time computation}, booktitle = {Proceedings of FOSSACS04}, pages = {27--41}, year = {2004}, volume = {2987}, series = {Lecture Notes in Computer Science}, publisher = {Springer} } @unpublished{DalLagoBaillot04, author = {Dal Lago, U. and Baillot, P.}, title = {On {L}ight {L}ogics, {U}niform {E}ncodings and {P}olynomial {T}ime}, note={ 11 pages, presented at the Workshop on Logics for Resources, Processes and Programs (LRPP'04) (affiliated with LICS 2004 and ICALP 2004)}, address={Turku, Finland}, month={July}, year={2004}, } @InProceedings{Laurent04a, author = {Olivier Laurent and Tortora de Falco, Lorenzo}, title = {Slicing polarized additive normalization}, booktitle = {Linear Logic in Computer Science}, editor = {Thomas Ehrhard and Jean-Yves Girard and Paul Ruet and Philip Scott}, volume = {316}, series = {London Mathematical Society Lecture Note Series}, publisher = {Cambridge University Press}, month = nov, year = {2004} } @Article{Laurent04b, author = {Olivier Laurent}, title = {Polarized games}, journal = {Annals of Pure and Applied Logic}, number = {1--3}, volume = {130}, pages = {79--123}, month = dec, year = {2004} } @Article{Laurent04cTA, author = {Olivier Laurent}, title = {Syntax vs. Semantics: a polarized approach}, journal = {Theoretical Computer Science}, year = {2004}, note = {To appear} } @Article{Laurent04dTA, author = {Olivier Laurent}, title = {Classical isomorphisms of types}, journal = {Mathematical Structures in Computer Science}, year = {2004}, note = {To appear} } @PHDTHESIS{Maurel04, AUTHOR = {F. Maurel}, TITLE = {Un cadre quantitatif pour la ludique}, SCHOOL = {Univ. Paris 7}, YEAR = {2004}, } @inproceedings{OHearn04, author="P. W. O'Hearn", title="Resources, Concurrency and Local Reasoning", pages="49-67", booktitle="Fifteenth International Conference on Concurrency Theory (CONCUR)", year="2004", address="London", month="September", series="LNCS", volume="3170", editor="P. Gardner and N. Yoshida", OPTnote= "{\bf APPSEM Themes D,H}", publisher ="Springer-Verlag, Berlin" } @inproceedings{OYR04, author = "P.W. O'Hearn and H. Yang and J.C. Reynolds", title = "Separation and Information Hiding", pages = "268--280", booktitle = "31st POPL", address = "Venice", month = "January", OPTnote= "{\bf APPSEM Themes A,D,H}", year = "2004" } @unpublished{PR04, author = "D. Pym and E. Ritter", title = "Reductive Logic and Proof Search: Proof Theory, Semantics and Control", note = "Volume 45, Oxford Logic Guides. Oxford University Press.", OPTnote = "{\bf APPSEM Theme F}", year = "2004" } @unpublished{POY04, author = "D. Pym and P. O'Hearn and H. Yang", note = "{\em Theoretical Computer Science}\/ 15(1).", OPTnote = "{\bf APPSEM Theme H}", title = "Possible worlds and resources: the semantics of {BI}", month="May", year = "2004" } @inproceedings{BCOP05, author = "R. Bornat and C. Calcagno and P.W. O'Hearn and M. Parkinson", title = "Permission Accounting in Separation Logic", booktitle = "32nd POPL", address = "Long Beach", month = "January", OPTnote= "{\bf APPSEM Themes D,H}", year = "2005" } @inproceedings{CGZ05, author = "C. Calcagno and P. Gardner and U. Zafarty", title = "Context Logic and Tree Update", booktitle = "32nd POPL", address = "Long Beach", month = "January", OPTnote= "{\bf APPSEM Themes G,H}", year = "2005" } @inproceedings{GW04, author = "P. Gardner and S. Maffeis", title = "Behavioural Equivalences for Dynamic Web Data", OPTnote= "{\bf APPSEM Themes G,H}", booktitle = "IFIP-TCS", year = "2005" } @inproceedings{FP04, author = "C. Fuhrmann and D. J. Pym", title = "On the Geometry of Interaction for Classical Logic", booktitle = "Proceedings of LICS", OPTnote= "{\bf APPSEM Theme H}", year = "2004" } @STRING{PROC = "Proc. of "} @STRING{MSCS = "Mathematical Structures in Computer Science"} @string{IC = "Information and Computation"} @string{FOSSACS = "Foundations of Software Science and Computation Structures (FOSSACS)"} @STRING{ICFP = "ACM International Conference on Functional Programming (ICFP)"} @STRING{LRPP= "Workshop on Logics for Resources, Processes, and Programs (LRPP)"} @STRING{FSTTCS= "Foundations of Software Technology and Theoretical Computer Science (FSTTCS)"} @STRING{PLANX = "Workshop on Programming Language Technologies for XML (PLAN-X)"} %theme H @Article{AehligJoachimski03a, author = {Klaus Aehlig and Felix Joachimski}, title = {Operational Aspects of Untyped Normalization by Evaluation}, journal = {Mathematical Structures in Computer Science}, volume = 14, number = 4, month = aug, theme = {C}, pages = {587--611}, year = 2004 } @inproceedings{DBLP:conf/icalp/EdalatP04, author = {Abbas Edalat and Dirk Pattinson}, title = {A Domain Theoretic Account of Picard's Theorem.}, booktitle = {ICALP}, theme={H}, year = {2004}, pages = {494-505}, ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3142{\&}spage=494}, crossref = {conf/icalp/2004}, bibsource = {DBLP, http://dblp.uni-trier.de} } @Article{abel:rairo04, author = {Andreas Abel}, title = {Termination Checking with Types}, journal = {RAIRO -- Theoretical Informatics and Applications}, year = 2004, key = {DOI: 10.1051/ita:2004015}, volume = 38, number = 4, pages = {277--319}, note = {Special Issue: Fixed Points in Computer Science (FICS'03)}, url = {http://www.edpsciences.org/articles/ita/abs/2004/04/ita0428NS/ita0428NS.html}, postscript = {http://www.tcs.informatik.uni-muenchen.de/\~{}abel/rairo04.ps.gz}, pdf = {http://www.edpsciences.org/articles/ita/pdf/2004/04/ita0428NS.pdf}, theme = {E} } @InProceedings{abelMatthes:csl04, author = {Andreas Abel and Ralph Matthes}, title = {Fixed Points of Type Constructors and Primitive Recursion}, booktitle = {Computer Science Logic, CSL'04}, pages = {190--204}, year = 2004, editor = {Jerzy Marcinkowski and Andrzej Tarlecki}, volume = 3210, series = lncs, publisher = springer, theme = {E} } @article(abelMatthesUustalu:fossacs03, author = {Andreas Abel and Raplh Matthes and Tarmo Uustalu}, title = {Iteration and Coiteration Schemes for Higher-Order and Nested Datatypes (Revised)}, journal=tcs, note = "to appear in FOSSACS'03 special issue", year = "2004", theme = {E} ) @INPROCEEDINGS(wirsingstatecharts, AUTHOR = "Diego Latella, Mieke Massink, Hubert Baumeister, and Martin Wirsing", TITLE = "Mobile UML statecharts", BOOKTITLE = " Proc. Global Computing", YEAR = "2004", editor = "C. Priami and P. Quaglia", publisher = "Springer LNCS") @inproceedings{wirsingamast, editor={Savitri Maharaj and others}, booktitle={Proc.\ AMAST 2004}, title={ Refining Mobile UML State Machines}, author = {Alexander Knapp and Stephan Merz and Martin Wirsing}, series = lncs, theme={D}, volume=3116, year = 2004} @proceedings{DBLP:conf/icwe/2004, editor = {Nora Koch and Piero Fraternali and Martin Wirsing}, title = {Web Engineering - 4th International Conference, ICWE 2004, Munich, Germany, July 26-30, 2004, Proceedings}, booktitle = {ICWE}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {3140}, year = {2004}, isbn = {3-540-22511-0}, crossref = {conf/icwe/2004}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings(johannsenSTACS04, author={Jan Johannsen}, title = "Satisfiability problems complete for deterministic logarithmic space", booktitle = "STACS 2004, 21st Annual Symposium on Theoretical Aspects of Computer Science, Proceedings. Springer LNCS 2996", editor = "Volker Diekert and Michel Habib", pages ="317-325", year=" 2004", theme={H}) @ARTICLE(HofmannScott04, AUTHOR = "Martin Hofmann and Phil Scott", TITLE = "Realizability models for BLL-like languages", YEAR = "2004", journal = tcs, volume=318, theme={H}, pages="121--137") @inproceedings{SannellaDT:mrg-overview04, author = {David Aspinall and Stephen Gilmore and Martin Hofmann and Donald Sannella and Ian Stark}, title = {Mobile Resource Guarantees for Smart Devices}, booktitle = {Proc.\ Intl.\ Workshop on Construction and Analysis of Safe, Secure and Interoperable Smart Devices (CASSIS 2004)}, location = {Marseille}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, year = 2004, pdf = {cassis2004.pdf}, theme = {H} } @Article(HSAB, AUTHOR={Klaus Aehlig and Ulrich Berger and Martin Hofmann and Helmut Schwichtenberg}, TITLE={An arithmetic for non-size-increasing polynomial-time computation}, journal=tcs, year=2004, volume=318) @inproceedings(csch, AUTHOR={Helmut Schwichtenberg and Peter Schuster}, TITLE={Constructive Solutions of Continuous Equations}, BOOKTITLE={One Hundred Years of Russell's Paradox}, PUBLISHER={De Gruyter}, EDITOR={G. Link}, YEAR=2004, THEME={B,I}) @inproceedings{programlogicgrail, author = {David Aspinall and Lennart Beringer and Martin Hofmann and Hans-Wolfgang Loidl and Alberto Momigliano}, title = {A Program Logic for Resource Verification}, booktitle = {Proceedings of 17th International Conference on Theorem Proving in Higher Order Logics (TPHOLs2004)}, location = {Park City, Utah}, publisher = {Springer-Verlag LNCS}, address = {Heidelberg}, series = {Lecture Notes in Computer Science}, volume = {}, pages = {}, year = {2004}, month = {September}, note = {To appear}, pdf = {tphol-paper.pdf} }@inproceedings{certgen, author = {Lennart Beringer and Martin Hofmann and Alberto Momigliano and Olha Shkaravska}, title = {Towards certificate generation for linear heap consumption}, booktitle = {Proceedings of ICALP/LICS Workshop on Logics for Resources, Processes, and Programs (LRPP2004)}, location = {Turku, Finland}, year = {2004}, month = {July}, publisher = {}, address = {}, journal = {}, volume = {}, pages = {}, note = {To appear}, pdf = {lrpp.pdf} } @STRING{PROC = "Proc. of "} @STRING{MSCS = "Mathematical Structures in Computer Science"} @string{IC = "Information and Computation"} @string{FOSSACS = "Foundations of Software Science and Computation Structures (FOSSACS)"} @STRING{ICFP = "ACM International Conference on Functional Programming (ICFP)"} @STRING{LRPP= "Workshop on Logics for Resources, Processes, and Programs (LRPP)"} @STRING{FSTTCS= "Foundations of Software Technology and Theoretical Computer Science (FSTTCS)"} @STRING{PLANX = "Workshop on Programming Language Technologies for XML (PLAN-X)"} %theme H @INPROCEEDINGS{DawGarGhe04-lrpp, author="A. Dawar and P. Gardner and G. Ghelli", title="Adjunct Elimination Through Games", booktitle = PROC # LRPP # ", Turku, Finland", year = 2004, theme = {H}, site = {pisa,imperial college} } @INPROCEEDINGS{DawGarGhe04-fsttcs, author="A. Dawar and P. Gardner and G. Ghelli", title="Adjunct Elimination Through Games in {S}tatic {A}mbient {L}ogic (Extended Abstract)", booktitle = PROC # "the 24th " # FSTTCS # ", Chennai, India", month = "December", Year = 2004, theme = {H}, site = {pisa,imperial college} } @UNPUBLISHED{DawGarGhe-complexity, author="A. Dawar and P. Gardner and G. Ghelli", title="Expressiveness and Complexity of Graph Logic", note="In preparation", theme = {H}, site = {pisa,imperial college} } @INPROCEEDINGS{ConGhe04-fossacs, author="G. Conforti and G. Ghelli", title="Decidability of Freshness, Undecidability of Revelation (Extended Abstract)", booktitle = PROC # FOSSACS # ", Barcelona, Spain", pages = "105--120", month = "March-April", year=2004, theme = {H}, site = {pisa} } @ARTICLE{CarGhe04-mscs, author = {L. Cardelli and G. Ghelli}, title = {{TQL}: A Query Language for Semistructured Data Based on the Ambient Logic}, journal = MSCS, volume = {14}, number = {3}, year = {2004}, issn = {0960-1295}, pages = {285--327}, publisher = {Cambridge University Press}, theme = {H}, site = {pisa,microsoft} } @INPROCEEDINGS{ColGheAl04-icfp, author = "D. Colazzo and G. Ghelli and P. Manghi and C. Sartiani", title = "Types for Path Correctness for {XML} Queries", booktitle = PROC # ICFP # ", Snowbird, Utah, USA", month = "September", year = 2004, theme = {H}, site = {pisa} } @INPROCEEDINGS{CGMS04-sebd, author = {G. Conforti and G. Ghelli and P. Manghi and C. Sartiani}, title = {A Self-organizing {XML} {P2P} Database System}, booktitle = PROC # "Dodicesimo Convegno su Sistemi Evoluti per Basi di Dati (SEBD), S.Margherita di Pula, Cagliari, Italy", pages = "394--401", year = 2004, theme = {H}, site = {pisa} } @INPROCEEDINGS{CS05-planx, author = {D. Colazzo and C. Sartiani}, title = {Typechecking Queries for Maintaining Schema Mappings in {XML} {P2P} Databases}, booktitle = PROC # PLANX, year = 2005, theme = {H}, site = {pisa} } %theme E -------------------------- @ARTICLE{ColGhe05-ic, author = "D. Colazzo and G. Ghelli", title = "Subtyping, Recursion and Parametric Polymorphism in {K}ernel {F}un", journal = IC, year = 2005, note = {To appear}, theme = {E}, site = {pisa} } %theme G @ARTICLE{CarGheGor05-ic, author="L. Cardelli and G. Ghelli and A. D. Gordon", title="Secrecy and Group Creation", journal = IC, year = 2005, note = {To appear}, theme = {G}, site = {pisa,microsoft} } % ---- 2004 -------------------------------------------------------------------- % ---- Journal Papers + Book chapters @article{BB04, author = "Barbosa, M. A. and Barbosa, L. S.", title = "A Relational Model for Component Interconnection", journal = "Journal of Universal Computer Science", year = "2004", volume = "10", number = "7", pages = "808--823", month = "July" } @incollection{WS04, author = "Barbosa, L. S. and Sun, M. and Aichernig, B. K. and Rodrigues, N.", title = "On the Semantics of Componentware: a Coalgebraic Perspective", booktitle = "Mathematical Frameworks for Component Software: Models for Analysis and Synthesis", editor = "Jifeng He and Zhiming Liu", series = "Series on Component-Based Development", publisher = "World Scientific", year = {(accepted)} } @article{MBtcs04, author = "Sun M., and Barbosa, L. S.", title = "Components as Coalgebras: the Refinement Dimension", journal = "Theoretical Computer Science, Elsevier", year = {(accepted)} } @Article{BFGPU:mscs2004, author = {G. Barthe and M.J. Frade and E. Gimenez and L. Pinto and T. Uustalu}, title = {Type-based termination of recursive definitions}, journal = {Mathematical Structures in Computer Science}, year = {2004}, volume = {14}, number = {1}, pages = {97-141} } % ---- Conference Papers @inproceedings{jno04, author = {J.N. Oliveira and C.J. Rodrigues}, title = {Transposing relations: from Maybe functions to hash tables}, booktitle = {Seventh International Conference on Mathematics of Program Construction, MPC'04}, year = {2004}, publisher = {Springer-verlag}, pages = {334-356}, volume = {3125}, series = {LNCS}, month = {July} } @inproceedings{esp04, author = {J.~Esp\'{\i}rito~Santo and L.~Pinto}, title = {Confluence and strong normalisation of the generalised multiary lambda-calculus}, booktitle = {International Workshop TYPES 2003 (revised papers)}, year = {2004}, publisher = {Springer-verlag}, editor = "Stefano Berardi, Mario Coppo, Ferruccio Damiani", volume = {3085}, series = {LNCS}, month = {May} } @inproceedings{BB04sblp, title = "Towards a Relational Model for Component Interconnection", author = "Barbosa, M. A. and Barbosa, L. S.", booktitle = "Proc. 8th Brazilian Symposium on Programming Languages", pages = "17--30", editor = "Lins, R. and Braga, C. and Chalub, F.", year = 2004, month = "May", address = "Niteroi, Brasil" } @inproceedings{MB04, author = "Sun M., and Barbosa, L. S.", title = "On Refinement of Generic Software Components", booktitle = "10th Int. Conf. Algebraic Methods and Software Technology ({AMAST})", editor = "Rettray, C. and Maharaj, S. and Shankland, C.", address = "Stirling", pages = "506--520", month = "August", publisher = "Springer Lect. Notes Comp. Sci. (3116)", year = 2004, note = "Best Student Co-authored Paper Award" } @inproceedings{SABZ04, author = "Sun M., and Aichernig, B. K. and Barbosa, L. S. and Naixiao, Z.", title = "A Coalgebraic Semantic Framework for Component Based Development in {UML}", booktitle = "Proc. Int. Conf. on Category Theory and Computer Science (CTCS'04)", editor = "Birkedal, L.", publisher = "{ENTCS} (to appear), Elsevier", month = "August", year = 2004 } @inproceedings{SZB04, author = "Sun M., and Naixiao, Z. and Barbosa, L. S.", title = "On Semantics and Refinement of {UML} Statecharts: A Coalgebraic View", booktitle = "Proc. of 2nd IEEE Int. Conf. on Software Engineering and Formal Methods", publisher = "IEEE Computer Society Press", pages = "164--173", editor = "Cuellar, J. and Liu, Z.", address = "Beijing, China", month = "September", year = 2004 } @inproceedings{BB04ictac, author = "Barbosa, M. A. and Barbosa, L. S.", title = "Specifying Software Connectors", booktitle = "1st International Colloquium on Theorectical Aspects of Computing ({ICTAC'04})", editor = "Araki, K. and Liu, Z.", address = "Guiyang, China", month = "September", publisher = "Springer Lect. Notes Comp. Sci. (to appear)", year = 2004 } @inproceedings{RB04, author = "Rodrigues, N. and Barbosa, L. S.", title = "Prototyping Behavioural Specifications in the {.Net} Framework", booktitle = "Proc. 7th Brazilian Symposium on Formal Methods (SBMF'2004)", publisher = "{ENTCS} (to appear), Elsevier", month = "November", year = 2004 } @inproceedings{Saraiva04, author = {João Saraiva}, title = "Design, Implementation and Animation of Spreadsheets in the Lrc System", booktitle = "Int. Workshop on Foundations of Spreadsheets (FoS'04)", editor = "Martin Erwig", publisher = "{ENTCS} (to appear), Elsevier", month = "September", year = 2004 } @inproceedings{VS04, title = "Tutorial on Strategic Programming Across Paradigms", author = "Joost Visser and João Saraiva", booktitle = "Proc. 8th Brazilian Symposium on Programming Languages", editor = "Lins, R. and Braga, C. and Chalub, F.", year = 2004, month = "May", address = "Niteroi, Brasil" } @inproceedings{CunhaA:makpfclp, title = "Making the {P}oint-free {C}alculus {L}ess {P}ointless", author = "A.~Cunha and J.~S. Pinto", booktitle = "Proc of the 2nd APPSEM II Workshop", pages = "178--179", year = 2004 } % ---- Thesis @PhdThesis{mjf:phd, author = {Maria Jo\~{a}o Frade}, title = {Type-Based Termination of Recursive Definitions and Constructor Subtyping in Typed Lambda Calculi}, school = {Universidade do Minho}, year = {2004} } % ----- Technical Report @techreport{PintoJS:genhs, author = "J.~A. Pinto", title = "Generalizing {H}ylo-shift", type = {Technical Report DI-PURe-04:10:01}, institution = { Departamento de Inform\'atica, Universidade do Minho}, month = {October}, year = 2004 } @article{GMP05, title="The Semantics of {BI }and Resource Tableaux", author="Didier Galmiche and Daniel M\'{e}ry and David Pym", journal="Math. Struct. Comp. Sci", volume="15", pages="1033--1088", year="2005" } @inproceedings{CP2, author = {M. Collinson and D. Pym}, title = {Bunching for Regions and Locations}, booktitle = {22nd MFPS, ENTCS 158}, pages = "171-197", year = 2006 } @unpublished{CPR1, author = {M. Collinson and D. Pym and E. Robinson}, title = {On Bunched Polymorphism}, note = {19th CSL: 36-50}, year = 2006 } @inproceedings{OHearn04, author = "P. W. O'Hearn ", note = "Extended version to appear in {\em Theoretical Computer Science}\/", title = "Resources, Concurrency and Local Reasoning", booktitle = "CONCUR'04: 15th International Conference on Concurrency Theory", address = "London", month = "August", publisher = {Springer}, series = {Lecture Notes in Computer Science}, pages="49--67", volume = {3170}, year = "2004" } Lu’s Caires, ƒtienne Lozes: Elimination of Quantifiers and Undecidability in Spatial Logics for Concurrency. CONCUR 2004: 240-257 @unpublished{CL04, author = "L. Caires and E. Lozes", note = "15th CONCUR, pp240-257", title = "Elimination of Quantifiers and Undecidability in Spatial Logics for Concurrency", year = "2004" } @unpublished{PB05, author = "M. Parkinson and G. Bierman", note = "32nd POPL", title = "Separation Logic and Abstraction", year = "2005" } @unpublished{BCO06, author = "C. Calcagno and J. Berdine and P. O'Hearn", note = "4th FMCO, LNCS 4111", title = "Smallfoot: Modular Automatic Assertion Checking with Separation Logic", year = "2006" } @unpublished{HJ03, author = "M. Hofmann and S. Jost", note = "30th POPL, pp185--197", title = "Static prediction of heap space usage for first-order functional programs", year = "2003" } @unpublished{H03, author = "M. Hofmann ", note = "Inf. Comput. 183(1), pp57--85", title = "Linear types and non-size-increasing polynomial time computation", year = "2003" } @unpublished{Caires04, author = {L Caires}, title = {{Behavioral and Spatial Observations in a Logic for the pi-Calculus}}, year = {2004}, note = {Proc. FoSSaCS: 72-89}} @article{POY04, author = "D. Pym and P. O'Hearn and H. Yang", title = "Possible Worlds and Resources: the semantics of {BI}", journal= "Theoretical Computer Science", volume = "315", number = "1", pages="257-305", year = "2004" } @unpublished{CC2, author = {L. Caires and L. Cardelli}, title = {{A spatial logic for concurrency (part II)}}, year = {2003}, note = {Theor. Comput. Sci. 322(3): 517-565}} @unpublished{CC1, author = {L. Caires and L. Cardelli}, title = {{A spatial logic for concurrency (part I)}}, year = {2003}, note = {Inf. Comput. 186(2): 194-235}} @unpublished{DGG03, author = {A. Dawar and P. Gardner and G. Ghelli}, title = {{Adjunct Elimination Through Games in Static Ambient Logic}}, year = {2004}, note = {24th FSTTCS, LNCS 3328, pp211-223}} @unpublished{ConG03, author = {G. Conforti and G. Ghelli}, title = {{Decidability of Freshness, Undecidability of Revelation}}, year = {2004}, note = {Proc. FoSSaCS: 105-120}} @unpublished{CG03, author = {L. Cardelli and G. Ghelli }, title = {{TQL: a query language for semistructured data based on the ambient logic}}, year = {2004}, note = {Mathematical Structures in Computer Science 14(3): 285-327}} @unpublished{CGG03, author = {L. Cardelli and P. Gardner and G. Ghelli }, title = {{Manipulating Trees with Hidden Labels}}, year = {2003}, note = {Proc. FoSSaCS, pp216-232 }} @unpublished{GM05, author = {P. Gardner and S. Maffeis}, title = {{Modelling Dynamic Web Data}}, year = {2005}, note = {Theoretical Computer Science 342(1), pp104-131 }} @unpublished{BCDO06, author = "J. Berdine and B. Cook and D. Distefano and P. O'Hearn", note = "18th CAV, to appear", title = "Automatic termination proofs for programs with shape-shifting heaps", year = "2006" } @InProceedings{CDOY06, author = {Cristiano Calcagno and Dino Distefano and Peter O'Hearn and Hongseok Yang}, title = {Beyond Reachability: {Shape} Abstraction in the Presence of Pointer Arithmetic}, booktitle = {13th SAS: Static Analysis Symposium}, OPTpublisher = {Springer}, series = {LNCS}, OPTvolume = {4134}, OPTpages = {182-203}, year = 2006, } @unpublished{GBC06, author = "A. Gotsman and J. Berdine and B. Cook", note = "13th SAS: Static Analysis Symposium. LNCS4134", title = "Interprocedural shape analysis with separated heap abstractions", year = "2006" } @InProceedings{BCOP05, author = "R. Bornat and C. Calcagno and P. O'Hearn and M. Parkinson ", pages = "59--70", title = "Permission Accounting in Separation Logic", booktitle ="32nd POPL", year = "2005", url = "http://www.dcs.qmul.ac.uk/~ohearn/papers/permissions_paper.pdf", } @InProceedings{CGZ05, author ="Calcagno, C. and Gardner, P. and Zarfaty, U.", title ="Context Logic and Tree Update", booktitle ="32nd POPL", year ="2005", pages ="271-282" } @inproceedings{ZG06, author = {U. Zarfaty and P. Gardner}, title = {Local Reasoning About Tree Update}, booktitle = {22nd MFPS, ENTCS 158}, pages = "399-424", year = 2006 } @unpublished{BCO04c, author = "J. Berdine and C. Calcagno and P. O'Hearn", note = "24th FSTTCS, LNCS 3328", pages="97--109", title = "A Decidable Fragment of Separation Logic", year = "2004" } @unpublished{DOY06, author = "D. Distefano and P. O'Hearn and H. Yang", note = "16th TACAS, LNCS 3920, pp287--302", title = "A local shape analysis based on separation logic", year = "2006" } @inproceedings{CGH05, author = {Calcagno, C. and Gardner, P. and Hague, M.}, title = {From Separation Logic to First-order Logic}, booktitle = {FOSSACS}, year = 2005 } @unpublished{MRG1, author = {D. Aspinall and S. Gilmore and M. Hofmann and D. Sannella and I. Stark}, title = {Mobile Resource Guarantees for Smart Devices}, year = {2004}, note = {CASSIS '04, LNCS 3362, pp.1Ð26}} @unpublished{MRG2, author = {{L. Beringer and K. MacKenzie and I. Stark}}, title = {Grail: a Functional Form for Imperative Mobile Code}, year = {2003}, month = {July}, note = {Proc. Found. Global Comp., ENTCS 85.1}} @unpublished{MRG3, author = {L. Beringer and M. Hofmann and A. Momigliano and O, Shkaravska}, title = {{Automatic Certification of Heap Consumption}}, year = {2004}, note = {Proc. LPAR, pp347-362 }} @unpublished{CCG05, author = {C. Calcagno and L. Cardelli and A. D. Gordon}, title = {Deciding validity in a spatial logic for trees}, year = {2005}, month = {July}, note = {Journal of Functional Programming}} @InProceedings{quviq-quickcheck, author = {Thomas Arts and John Hughes and Joakim Johansson and Ulf Wiger}, title = {Testing Telecoms Software with {Quviq QuickCheck}}, booktitle = {Fifth ACM SIGPLAN Erlang Workshop}, year = 2006, editor = {Phil Trinder}, address = {Portland, Oregon}, month = {September}, publisher = {ACM SIGPLAN} } @InProceedings{BDJRS06, author = {Adam Biltcliffe and Michael Dales and Sam Jansen and Thomas Ridge and Peter Sewell}, title = {Rigorous Protocol Design in Practice: An Optical Packet-Switch {MAC} in {HOL}}, booktitle = {Proc.~ICNP, The 14th IEEE International Conference on Network Protocols}, year = 2006, month = nov, note = {To appear. \url{http://www.cl.cam.ac.uk/users/pes20/optical/root.pdf}} } @Unpublished{Lassen-Stoevring:06, author = "Kristian Støvring and Søren Lassen", title = "A Complete, Co-Inductive Syntactic Theory of Sequential Control and State", note = "To appear as a BRICS research report", year = 2006, month = Jul } @INPROCEEDINGS(a, AUTHOR = "Nick Benton and Andrew Kennedy and Martin Hofmann and Lennart Beringer", TITLE = "Reading Writing and Relations", BOOKTITLE = "Proc. APLAS 2006", YEAR = "2006", note = "to appear" ) @STRING{PROC = "Proc. of "} @STRING{LNCS = "LNCS"} @STRING{MSCS = "Mathematical Structures in Computer Science"} @STRING{DATAX = "Workshop on Database Technologies for Handling XML Information on the Web (DataX)"} @STRING{PLANX = "Workshop on Programming Language Technologies for XML (PLAN-X)"} @STRING{DBPL = "Data Base Programming Languages (DBPL)"} @string{IC = "Information and Computation"} @string{JFP = "Journal of Functional Programming (JFP)"} @ARTICLE{CarGhe04-mscs, author = {L. Cardelli and G. Ghelli}, title = {{TQL}: A Query Language for Semistructured Data Based on the Ambient Logic}, journal = MSCS, volume = {14}, number = {3}, year = {2004}, issn = {0960-1295}, pages = {285--327}, publisher = {Cambridge University Press}, theme = {H}, site = {pisa,microsoft} } @INPROCEEDINGS{GheReSim06-datax, author = "Giorgio Ghelli and Christopher R\'e and J\'er\^ome Sim\'eon", title = "{XQuery!}: An {XML} Query Language With Side Effects", booktitle = PROC # DATAX, series = LNCS, year = 2006, note = "To appear", theme = {H}, site = {pisa} } @unpublished{GheRosSim06, author = "Giorgio Ghelli and Kristoffer Rose and J\'er\^ome Sim\'eon", title = "Commutativity Analysis in {XML} Update Languages", year = 2006, note = "Submitted" } @unpublished{Galax, title = "Galax", year = 2006, note = "{http://www.galaxquery.org/}" } @INPROCEEDINGS{CarGarGhe06, author="L. Cardelli and P. Gardner and G. Ghelli", title="Manipulating Trees with Hidden Labels", note = "To appear", theme = {H}, year=2006 } @ARTICLE{CarGheGor05-ic, author="L. Cardelli and G. Ghelli and A. D. Gordon", title="Secrecy and Group Creation", journal = IC, volume = {196}, number = {2}, year = {2005}, pages = {127--155}, theme = {E,G}, site = {pisa,microsoft} } %% HWL was here @InProceedings{laud05:_type, author = {P. Laud and T. Uustalu and V. Vene}, title = {Type systems equivalent to dataflow analyses for imperative languages}, booktitle = {{3rd APPSEM II Workshop (APPSEM '05)}}, year = 2005, address = {Frauenchiemsee, Germany}, month = sep, note = {To appear in TCS}, url = {http://www.cs.ioc.ee/~tarmo/papers/appsem05-tcs.pdf}, } @inproceedings{PR05, author = {D. Pym and E. Ritter}, title = {A game semantics of reductive proof search}, booktitle = {Workshop on Games for Logic and Programming Languages}, note= "Edinburgh, April", year = 2005 } @InProceedings{LoWo06, author = {Longley, John and Wolverson, Nicholas}, title = {{Game semantics for object-oriented languages: a progress report}}, booktitle = {Games for Logic and Programming Languages II (GaLoP II)}, address = {Seattle, Washington}, month = aug, year = 2006, url = {http://homepages.inf.ed.ac.uk/jrl/Research/galop.pdf} } @article{CurPan, author = {Pierre-Louis Curien and Hugo Herbelin}, title = {Abstract machines for dialogue games}, year = {2005}, note = {To appear in `Interactive models of computation and program behaviour, collection ``Panoramas et Synth\`eses of the Soci\'et\'e Math\'ematique de France} } @InProceedings{cheney:scrap-nameplate, author = {James Cheney}, title = {Scrap your Nameplate}, booktitle = {ICFP 2005: Proceedings of the Tenth ACM SIGPLAN International Conference on Functional programming}, year = 2005, pages = {180--191}, publisher = {ACM Press}, url = {http://doi.acm.org/10.1145/1086365.1086389} }