@STRING{PROC = "Proc. of "} @STRING{LNCS = "LNCS"} @STRING{SV = "Springer-Verlag"} @STRING{SVADDRESS = "Berlin"} @string{FOSSACS = "Foundations of Software Science and Computation Structures (FOSSACS)"} @STRING{ICALP = "International Colloquium on Automata, Languages, and Programming (ICALP)"} @string{lncs = "Lecture Notes in Computer Science"} @string{springer = "Springer-Verlag"} @string{acm = "ACM Press"} @string{jfp = "Journal of Functional Programming"} @string{mscs = "Mathematical Structures in Computer Science"} @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)"} @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"} @string{ESOP2004 = "Programming Languages \& Systems, 13th European Symp.\ Programming"} @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{EdaPat, author={ A. Edalat and D. Pattinson}, title={Initial Value Problems in Domain Theory}, booktitle={Proc. International Conference on Computability and Complexity in Analysis (CCA 2003)}} @inproceedings{Pat, author={D. Pattinson}, title={Computable Functions on Final Coalgebras}, editor={H.-Peter Gumm}, booktitle={Coalgebraic Methods in Computer Science (CMCS 2003)}} @InProceedings{GrailLogic, author = {Aspinall, D. and Beringer, L. and Hofmann, M. and Loidl, H-W. and Momigliano, A.}, title = {{A Resource-aware Program Logic for Grail}}, booktitle = {Technical Report}, year = 2004, note = {\url{www.dcs.ed.ac.uk/home/mrg}} } @InProceedings{JoHo03, author = {Hofmann, M. and Jost, S.}, title = {{Static Prediction of Heap Space Usage for First-Order Functional Programs}}, booktitle = {POPL'03 --- Symposium on Principles of Programming Languages}, year = 2003, address = {New Orleans, LA, USA}, month = jan, publisher = {ACM Press}, abstract = "We show how to efficiently obtain linear a priori bounds on the heap space consumption of first-order functional programs. The analysis takes space reuse by explicit deallocation into account and also furnishes an upper bound on the heap usage in the presence of garbage collection. It covers a wide variety of examples including, for instance, the familiar sorting algorithms for lists, including quicksort. The analysis relies on a type system with resource annotations. Linear programming (LP) is used to automatically infer derivations in this enriched type system. We also show that integral solutions to the linear programs derived correspond to programs that can be evaluated without any operating system support for memory management. The particular integer linear programs arising in this way are shown to be feasibly solvable under mild assumptions." } @misc{Jo04,author="Steffen Jost",title={LFD\_infer: an implementation of static heap space inference}, text={Presented at the workshop SPACE'04, Venice January 2004, see also \url{www.tcs.informatik.uni-muenchen.de/~jost}}, year=2004} @INPROCEEDINGS{CarGarGhe02-icalp, author="L. Cardelli and P. Gardner and G. Ghelli", title="A Spatial Logic for Querying Graphs", booktitle = PROC # "the 29th " # ICALP # ", Malaga, Spain", month = "July", year=2002, series = LNCS, number = 2380, pages = "597-610", address = SVADDRESS, publisher = SV, eds = "P. Widmayer and F. T. Ruiz and R. Morales and M. Hennessy and S. Eidenbenz and R. Conejo" } @UNPUBLISHED{DawGarGhe-complexity, author="A. Dawar and P. Gardner and G. Ghelli", title="Expressiveness and Complexity of Graph Logic. In preparation" } @UNPUBLISHED{DawGarGhe-games, author="A. Dawar and P. Gardner and G. Ghelli", title="Adjunct Elimination through Games. In preparation" } @InProceedings{Caires::fossacs::04, author = {L. Caires}, title = {Behavioral and Spatial Properties in a Logic for the Pi-Calculus}, booktitle = {Proc. of Foundations of Software Science and Computation Structures'2004}, year = 2003, series = {Lecture Notes in Computer Science}, editor={Igor Walukiwicz}, publisher={Springer Verlag}, abstract={In addition to behavioral properties, spatial logics can talk about other key properties of concurrent systems like secrecy, freshness, usage of resources, and distribution. In this work we study an expressive spatial logic for systems specified in the synchronous Pi-calculus with recursion, based on a small set of behavioral and spatial observations. We give coinductive and equational characterizations of the equivalence induced on processes by the logic, and conclude that it strictly lies between structural congruence and strong bisimulation. We also show that model-checking is decidable for a useful class of processes that includes the finite-control fragment of the Pi-calculus.}, note={A preliminary version of this work was presented at the APPSEM Workshop on Spatial Logics, Nottingham, UK, March 2003} } @Article{caires.cardelli:part-i-tcs, author = "L. Caires and L. Cardelli", title = "{A Spatial Logic for Concurrency (Part II)}", journal = "Theoretical Computer Science", Year={to appear}, abstract={We present a modal logic for describing the spatial organization and the behavior of distributed systems. In addition to standard logical and temporal operators, our logic includes spatial operations corresponding to process composition and name hiding, and a fresh name quantifier. In Part I of this work we study the fundamental semantic properties of our logic; the focus of the present Part II is on proof theory. The main contributions are a sequent-based proof system for our logic, and a proof of cut-elimination for its first-order fragment.}} @Article{caires.cardelli:part-i-ic, author = "L. Caires and L. Cardelli", title = "{A Spatial Logic for Concurrency (Part I)}", journal = "Information and Computation", Year={2003}, pages="194--235", volume=186, number=2, abstract={We present a logic that can express properties of freshness, secrecy, structure, and behavior of concurrent systems. In addition to standard logical and temporal operators, our logic includes spatial operations corresponding to composition, local name restriction, and a primitive fresh name quantifier. Properties can also be defined by recursion; a central aim of this paper is then the combination of a logical notion of freshness with inductive and coinductive definitions of properties.}} @INPROCEEDINGS{ConGhe04-fossacs, author="G. Conforti and G. Ghelli", title="Decidability of Freshness, Undecidability of Revelation (Extended Abstract)", booktitle = PROC # FOSSACS # ", Barcelona, Spain", month = "March-April", year=2004 } @inproceedings{BFG04:SemanticsForWebServicesAuthentication, author="K. Bhargavan and C. Fournet and A. D. Gordon", title = {A Semantics for Web Services Authentication}, booktitle="31st ACM Symposium on Principles of Programming Languages (POPL'04)", year=2004, pages="198--209"} @unpublished{mackenziewolverson:camelot03, author = "Kenneth MacKenzie and Nicholas Wolverson", title = "{Camelot} and {Grail}: Compiling a Resource-Aware Functional Language for the {Java} Virtual Machine", note = "Paper presented at \emph{IFL 2003: 15th International Workshop on the Implementation of Functional Languages}", month = sep, year = 2003, url = "http://www.macs.hw.ac.uk/~ifl03/" } @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", year = "2004" } @inproceedings{BTR04, author = "L. Birkedal and N. Topr-Smith and J.C. Reynolds", title = "Local Reasoning about a Copying Garbage Collector", pages = "220--231", booktitle = "31st POPL", address = "Venice", month = "January", year = "2004" } @inproceedings{Bean03, author = "J. Bean", title = "Ribbon Proofs", pages = "??--??", booktitle = "Proceedings of the 19th MFPS Conference", address = "Montreal", month = "March", year = "2003" } @inproceedings{GM03, author = "P. Gardner and S. Maffeis", title = "Modelling Dynamic Web Data", booktitle = "International Conference on Databases and Programming Languages", address = "Berlin", note= "Springer LNCS 2921, 17 pages", year = "2003" } @inproceedings{CGG03, author = "L. Cardelli and P. Gardner and G. Ghelli", title = "Manipulating Trees with Hiding'", booktitle = "International Conference on Foundations of Software Science and Computational Structures", address = "Warsaw", note= "Springer LNCS 2620, 15 pages", year = "2003" } @inproceedings{BBG03, author = "P. Buneman and G. Bierman and P. Gardner", title = "Ubiquitous Data'", booktitle = "Ubinet workshop", note= "2 pages", year = "2003" } @unpublished{POY04, author = "D. Pym and P. O'Hearn and H. Yang", note = "To appear in {\em TCS}\/ ", title = "Possible worlds and resources: the semantics of {BI}", year = "2004" } @unpublished{GMP04, author = "D. Galmiche and D. Mery and D. Pym", note = "Submitted", title = "Resource Tableaux", year = "2004" } @InProceedings{beringer/mackenzie/stark:graffi, author = {Beringer and MacKenzie and Stark}, title = {Grail: a Functional Form for Imperative Mobile Code}, booktitle = {Foundations of Global Computing: Proceedings of the 2nd~EATCS Workshop}, year = 2003, series = {Electronic Notes in Theoretical Computer Science}, publisher = {Elsevier}, month = jun, url = {http://www.ed.ac.uk/~stark/graffi.html} } @InProceedings{aspinall+:bytecodelogic03, author = {David Aspinall, Lennart Beringer, Martin Hofmann and Hans-Wolfgang Loidl}, title = {A resource-aware program logic for a {JVM}-like 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/proceedings} } @Misc{atkey:separation, author = {Robert Atkey}, title = {A Calculus for Resource Relationships}, howpublished = {Short paper presented at \emph{SPACE 2004: Second workshop on Semantics, Program Analysis, and Computing Environments for Memory Management}}, month = jan, year = 2004, url = {http://www.diku.dk/topps/space2004/} } @STRING{LNCS = {Lecture Notes in Computer Science}} @STRING{SPRINGER = {Springer-Verlag}} @STRING{ACM = {ACM Press}} @inproceedings{effectspopl03, author = {Hayo Thielecke}, title = {From Control Effects to Typed Continuation Passing}, booktitle = {30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'03)}, publisher = {ACM}, pages = {139--149}, year = 2003, } @inproceedings{answertypecbn, author = {Hayo Thielecke}, title = {Answer Type Polymorphism in Call-by-name Continuation Passing}, booktitle = {European Symposium on Programming (ESOP)}, year = 2004, publisher = {Springer Verlag} } @INPROCEEDINGS{LeBotlan-Remy-ICFP, AUTHOR = {{Le Botlan}, Didier and R{\'e}my, Didier}, TITLE = {{MLF}: Raising {ML} to the power of System-{F}}, BOOKTITLE = {Proceedings of the Eighth {ACM SIGPLAN} International Conference on Functional Programming}, PAGES = {27--38}, YEAR = 2003, MONTH = AUG, URL = {http://pauillac.inria.fr/~remy/work/mlf/icfp.pdf}, ABSTRACT = { We propose a type system {MLF} that generalizes {ML} with first-class polymorphism as in System~{F}. Expressions may contain second-order type annotations. Every typable expression admits a principal type, which however depends on type annotations. Principal types capture all other types that can be obtained by implicit type instantiation and they can be inferred. All expressions of ML are well-typed without any annotations. All expressionsof System~{F} can be mechanically encoded into {MLF} by dropping all type abstractions and type applications, and injecting types of lambda-abstractions into {MLF} types. Moreover, only parameters of lambda-abstractions that are used polymorphically need to remain annotated. } } @UNPUBLISHED{DiCosmo-Pottier-Remy-subiso, AUTHOR = {{Di Cosmo}, Roberto and Fran\c{c}ois Pottier and Didier R{\'e}my}, TITLE = {Subtyping Recursive Types modulo Associative Commutative Products}, NOTE = {Draft paper}, YEAR = {2003}, ABSTRACT = { This work sets the formal bases for building tools to retrieve classes in object-oriented libraries. In such systems, the user provides a query, formulated as a set of class interfaces, and the tool returns classes in the library that can be used to implement the user's request and automatically builds the corresponding adaptation code. Recursive types model object-oriented features and subtyping of recursive types allows to account for structural subtyping in object-oriented programming languages. 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 query formulated by the user and the answers retrieved by the tool. We show that this relation is a composition of the usual 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. }, URL = {http://pauillac.inria.fr/~remy/work/dicosmo-pottier-remy-03.ps.gz} } @INPROCEEDINGS{Simonet-APLAS, AUTHOR = {Vincent Simonet}, TITLE = {Type inference with structural subtyping: A faithful formalization of an efficient constraint solver}, YEAR = {2003}, MONTH = NOV, BOOKTITLE = {Programming Languages and Systems, first Asian Symposium, APLAS 2003}, EDITOR = {Atsushi Ohori}, SERIES = LNCS, PUBLISHER = SPRINGER, NUMBER = 2895, PAGES = {283--302}, ABSTRACT = {We are interested in type inference in the presence of structural subtyping from a pragmatic perspective. This work combines theoretical and practical contributions: first, it provides a faithful description of an efficient algorithm for solving and simplifying constraints; whose correctness is formally proved. Besides, the framework has been implemented in Objective Caml, yielding a generic type inference engine. Its efficiency is assessed by a complexity result and a series of experiments in realistic cases.} } @INPROCEEDINGS{Simonet-ICFP, AUTHOR = {Vincent Simonet}, TITLE = {An Extension of {HM(X)} with Bounded Existential and Universal Data-Types}, MONTH = AUG, YEAR = 2003, BOOKTITLE = {Proceedings of the 8th ACM SIGPLAN International Conference on Functional Programming (ICFP 2003)}, PAGES = {39--50}, ADDRESS = {Uppsala, Sweden}, PUBLISHER = {ACM Press} } @INPROCEEDINGS{Pottier-LICS, AUTHOR = {Fran\c{c}ois Pottier}, TITLE = {A Constraint-Based Presentation and Generalization of Rows}, URL = {http://pauillac.inria.fr/~fpottier/publis/fpottier-lics03.ps.gz}, BOOKTITLE = {Eighteenth Annual {IEEE} Symposium on Logic In Computer Science (LICS'03)}, PAGES = {331--340}, ADDRESS = {Ottawa, Canada}, MONTH = JUN, YEAR = {2003}, ABSTRACT = {We study the combination of possibly conditional non-structural subtyping constraints with rows. We give a new presentation of rows, where row terms disappear; instead, we annotate constraints with \emph{filters}. We argue that, in the presence of subtyping, this approach is simpler and more general. In the case where filters are finite or cofinite sets of row labels, we give a constraint solving algorithm whose complexity is $O(n^3m\log m)$, where $n$ is the size of the constraint and $m$ is the number of row labels that appear in it. We point out that this allows efficient type inference for record concatenation. Furthermore, by varying the nature of filters, we obtain several natural generalizations of rows.} } @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} } @inproceedings{Barthe-Cirstea-Kirchner-Liquori, author={G. Barthe, H. Cirstea, C. Kirchner and L. Liquori}, title={Pure Pattern Type Systems}, booktitle={Proceedings of POPL'03}, year={2003}, editor={ACM Press} } @UNPUBLISHED{2003-DiCosmo-Pottier-Remy-subiso, AUTHOR = {{Di Cosmo}, Roberto and Fran\c{c}ois Pottier and Didier R{\'e}my}, TITLE = {Subtyping Recursive Types modulo Associative Commutative Products}, NOTE = {Draft paper}, YEAR = {2003}, URL = {http://pauillac.inria.fr/~remy/work/dicosmo-pottier-remy-03.ps.gz} } @misc{bierman-sigmod2003, title={Formal semantics and analysis of object queries}, author={G. Bierman}, note={Proceedings of ACM SIGMOD 2003. Pages 407-418}, year=2003} @misc{sewell-ICFP2003, author={James Leifer and Gilles Peskine and Peter Sewell and Keith Wansbrough}, title={Global abstraction-safe marshalling with hash types}, note={In ICFP 2003}, year=2003} @misc{hyland-TCS, author={M. Hyland and G. Plotkin and J. Power}, title={Combining Effects: Sum and Tensor}, note={Accepted by Theoretical Computer Science}, year=2003} @misc{hyland-CW2004, author={M. Hyland and P. Levy and G. Plotkin and J. Power}, title={Combining continuations with other effects}, note={Accepted to appear in Continuations Workshop 2004}, year=2003} \bibitem N. Gambino and M. Hyland. Well-founded Trees and Dependent Polynomial Functors. Draft paper. @misc{fiore-POPL2004, author={M.P.Fiore}, title={Isomorphisms of generic recursive polynomial types}, note={Accepted to appear in POPL 2004}, year=2003} @misc{bal, author={V.Balat and R.Di Cosmo and and M.P.Fiore}, title={Extensional normalisation and typed-directed partial evaluation for typed lambda calculus with sums}, note={Accepted to appear in POPL 2004}, year=2003} @misc{bal2, author={M.P.Fiore and R.Di Cosmo and V. Balat}, title={Remarks on isomorphisms in typed lambda calculi with empty and sum types}, note={Accepted to appear in the Annals of Pure and Applied Logic}, year=2003} @misc{Pinto-TLCA2003, author={J.~Esp\'{\i}rito~Santo and L.~Pinto}, title={Permutative conversions in intuitionistic multiary sequent calculi with cuts}, note={In M.~Hofmann, ed., Proc.\ of 6th Conf. on Typed Lambda Calculi and Applications, v.~2701, LNCS, pp.~286--300. Springer-Verlag, Berlin}, year=2003} @misc{Pinto-TYPES2003, author={J.~Esp\'{\i}rito~Santo and L.~Pinto}, title={Confluence and strong normalisation of the generalised multiary lambda-calculus. Accepted for publication in the Proc. of TYPES 2003 to be published as a LNCS volume}, year=2003} @misc{Frade-thesis2003, author={M. Jo\~{a}o Frade}, title={"Type-Based Termination of Recursive Definitions and Constructor Subtyping in Typed Lambda Calculi"}, note={Ph.D. thesis}, year=2003} @PhdThesis{makholm-thesis-2003, author = {Makholm, Henning}, title = {A language-independent framework for region inference}, school = {DIKU, University of Copenhagen}, year = {2003}, OPTkey = {}, OPTtype = {}, OPTaddress = {}, month = {August}, OPTnote = {}, OPTannote = {} } % 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"} @article{ReusStr:TCS, author = {B.~Reus and Th.~Streicher}, title = "Semantics and Logics of Object Calculi", journal = {TCS}, volume = "?", number = "?", year = 2004 , note = "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} } % 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{\"o}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) @misc{Qioa, author={H. Qiao}, title={Testing and Proving in Dependent Type Theory}, note={PhD thesis, Chalmers University of Technology}, year=2003} @misc{Check03, author={P. Dybjer and H. Qiao and M. Takeyama}, title={Verifying Haskell programs by combining testing and proving}, note={in Proceedings of the 3rd International Conference on Quality Software, Dallas, November 2003. IEEE Computer Society, 272-279.}, year=2003} @misc{Gen03, author={M. Benke and P. Dybjer and P.Jansson}, title={Universes for generic programs and proofs in dependent type theory}, note={Nordic Journal of Computing 10 (2003), 1-25}, year=2003} @inproceedings{AGMO, author="S. Abramsky, D. Ghica, A. Murawski and L. Ong", title="Applying Game Semantics to Compositional Software Modeling and Verifications", booktitle="TACAS 2004, Tenth International Conference on Tools and Algorithms for the Construction and Analysis of System", month="March", year="2004", series="LNCS", publisher="Springer Verlag", } @inproceedings{Ghi, author="D. Ghica", title="Semantical Analysis of Noninterference 3: An Operational Approach", booktitle="ESOP 2004, The European Symposium on Programming", month="March", year="2004", series="LNCS", publisher="Springer Verlag", } @inproceedings{GM, author="D. Ghica and A. Murawski", title="Angelic Semantics of Fine-Grained Concurrency", booktitle="FOSSACS: Foundations of Software Science and Computation Structures", month="March", year="2004", series="LNCS", publisher="Springer Verlag", } @Unpublished{Mellies:asynchronous1, author = {Paul-Andr\'e Melli\`es}, title = {Asynchronous games 1: an orbital formulation of arena games}, year = {2003}, note = {Submitted to \textit{Mathematical Structure in Computer Science}}, DMI-CATEGORY = {subm}, DMI-STATUS = {}, wwwwlink = {}, DMI-TIME = {}, X-LABINTEL = {PUB} } @article{Hyland-Schalk, author = {M. Hyland and A. Schalk}, title = {Glueing and Orthogonality for Models of Linear Logic}, journal = {Theoretical Computer Science}, volume = {294}, pages = {183-231}, year = 2003} @Inproceedings{Laird-csl03,author = "J. Laird",title = "Bistability: an extensional characterization of sequentiality",booktitle = "Proceedings of CSL '03",publisher = "Springer",series = "LNCS",number = 2803,year = 2003} @article{CurLairdSa, author = {P.-L. Curien}, title = {Sequential algorithms as bistable maps}, note = {draft}, year = 2003} @misc{Str03, author = {T. Streicher}, title = {Laird Domains}, note = {unpublished notes available at $\mathtt{http{:}{/}{/}www.mathematik.tu-darmstadt.de{/} \tilde{\;}streicher/LD.ps.gz}$}, year = {2003}} @misc{Rec03, author={ T. Coquand and R. Pollack and M. Takeyama}, title ={A logical framework with dependently typed records}, note={In Typed Lambda Calculus and Applications, TLCA'03, volume 2701 of LNCS. Springer-Verlag}, year=2003} @InProceedings(Hannay-2003, Author = "Hannay, J. and Katsumata, S. and Sannella, D.", Title = "Semantic and syntactic approaches to simulation relations", BookTitle = "28th Intl. Symp. on Mathematical Foundations of Computer Science", Organization = "Springer-Verlag", Pages = "68-91", Year = "2003", Note = "(invited paper)" ) @Book(CASL-manual, Author = "Bidoit, M. and Mosses, P.", Title = "\textsc{Casl} User Manual", Publisher = "Springer-Verlag", Series = "LNCS", Volume = "2900", Year = "2003" ) @InCollection(Sannella-Tarlecki-2003, Author = "Sannella, D. and Tarlecki, A.", Title = "Foundations", Crossref = "CASL-manual", BookTitle = "\textsc{Casl} User Manual", Chapter = "10", Year = "2003" ) @InProceedings(Mijajlovic-Torp-Smith-2004, Author = "Mijajlovic, I. and Torp-Smith, N.", Title = "Refinement in Separation Context", BookTitle = "SPACE 2004", Organization = "ACM", Year = "2004" ) @InProceedings(OHearn-Yang-Reynolds-2004, Author = "O'Hearn, P. W. and Yang, H. and Reynolds, J. C.", Title = "Separation and Information Hiding", BookTitle = "Principles of Programming Languages", Organization = "ACM", Year = "2004" ) @InProceedings(Bean-2003, Author = "Bean, J.", Title = "Ribbon Proofs", BookTitle = "19th Conference on Math. Foundations of Programming Semantics", Year = "2003" ) @InProceedings(Torp-Smith-2004, Author = "Birkedal, L. and Torp-Smith, N. and Reynolds, J. C.", Title = "Local Reasoning about a Copying Garbage Collector", BookTitle = "Principles of Programming Languages", Organization = "ACM", Year = "2004" ) @InProceedings(Biri-Galmiche-2003, Author = "Biri, Nicolas and Galmiche, D.", Title = "A Separation Logic for Resource Distribution", BookTitle = "Foundations of Software Technology and Theoretical Computer Science", Organization = "Springer-Verlag", Year = "2003" ) @Unpublished(Reddy-SPACE-2004, Author = "Reddy, U. S.", Title = "Semantic Modelling of Storage", Note = "Invited talk at SPACE 2004 Workshop", Year = "2004" ) @Article(Reus-Streicher-TCS, Author = "Reus, B. and Streicher, T.", Title = "Semantics and Logics of Object Calculi", Journal = "Theoretical Computer Science", Pages = "(to appear)", Year = "2004" ) @InProceedings(Benton-2004, Author = "Benton, N.", Title = "Simple Relational Correctness Proofs for Static Analyses and Program Transformations", BookTitle = "Principles of Programming Languages", Organization = "ACM", Year = "2004" ) @Unpublished(RS04, Author = "Rosolini, G. and Simpson, A.", Title = "Using Synthetic Domain Theory to Prove Operational Properties of a Powerful Polymorphic Language", Note = "(manuscript)", Year = "2004" ) @Misc{BucaloA:confft, author = {A. Bucalo and G. Rosolini}, title = {Continuous functions in formal topology}, year = {2003}, note = {Submitted for publication} } @Misc{BirkedalL:catrg, author = {L. Birkedal and G. Rosolini}, title = {Categories of reflexive graphs}, year = {2004}, note = {in preparation} } @InProceedings(Abbot-2003, Author = "Michael Abbott and Thorsten Altenkirch and Neil Ghani", Title = "Categories of Containers", BookTitle = "FOSSACS", Organization = "Springer-Verlag", Year = "2003" ) @InProceedings(Abbot-2003-derivatives, Author = "Michael Abbott and Thorsten Altenkirch and Neil Ghani and Conor McBride", Title = "Derivatives of Containers", BookTitle = "TLCA", Organization = "Springer-Verlag", Year = "2003" ) @Misc(SS04, Author = "Schoepp, U. and Stark, I.", Title = "A Bunched Dependent Type Theory for Programming and Reasoning with Names and Binding", HowPublished = "(in preparation)" ) @InProceedings(Barbosa-Oliveira-CMCS-2003, Author = "Barbosa, L. and Oliveira,J. ", Title = "Software Components Made Generic", BookTitle = "CMCS '03", Organization = "Elsevier", Year = "2003", Note = "(to appear as ENTCS)" ) @Misc(Crole-2003, Author = "Crole, R.", Title = "Basic Category Theory for Models of Syntax", HowPublished = "Generic Programming International Summer School, 2003" ) @InProceedings(Fiadeiro-2003, Author = "Fiadeiro, J.", Title = "Coordination Technologies for Just-in-time Integration", BookTitle = "Formal Methods at the Crossroads", Year = "2003" ) @InProceedings(Fiadeiro-Lopes-Wermelinger-2003, Author = "Fiadeiro, J. and Lopes, A. and Wermelinger, M.", Title = "A Mathematical Semantics for Architectural Connectors", BookTitle = "Generic Programming", Year = "2003" ) @InProceedings(Andrade-2003, Author = "Luis Andrade and Jose Fiadeiro and Antonia Lopes and Micehl Wermelinger", Title = "Architectural Techniques for Evolving Control Systems", BookTitle = "Formal Methods for Railway Operation and Control Systems", Year = "2003" ) @Article(Lopes-2003, Author = "Antonia Lopes and Michel Wermelinger and Jose Fiadeiro", Title = "Higher-Order Architectural Connectors", Journal = "Transactions on Software Engineering Methodology", Year = "2003" ) @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 } @ARTICLE{ResVic, AUTHOR={Resende, Pedro and Vickers, Steven}, TITLE={Localic Sup-lattices and Tropological Systems}, ISSN={0304-3975}, JOURNAL={Theoretical Computer Science}, VOLUME={305}, YEAR={2003}, PAGES={311--346} } @ARTICLE{UniCharPP, AUTHOR={Vickers, S.J. and Townsend, C.F.}, TITLE={A Universal Characterization of the Double Powerlocale}, JOURNAL={Theoretical Computer Science}, ISSN={0304-3975}, NOTE={accepted for publication}, YEAR={2003} } @ARTICLE{EntSys, AUTHOR={Vickers, S.J.}, TITLE={Entailment Systems for Stably Locally Compact Locales}, JOURNAL={Theoretical Computer Science}, ISSN={0304-3975}, NOTE={accepted for publication}, 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} } @InCollection{Eda03a, author = {Edalat, A.}, title = {An extension of {G}leason's theorem for quantum computation}, booktitle = {quant-ph/0311070 (electronic archive)}, publisher = {arXiv}, year = 2003 } @Unpublished{jung03, author = {A. Jung}, title = {Stably compact spaces and the probabilistic powerspace construction}, note = {Under review for ENTCS vol.\ 87}, year = 2003 } @Unpublished{alvarez03, author = {M. Alvarez-Manilla and A. Jung and K. Keimel}, title = {The probabilistic powerdomain for stably compact spaces}, note = {23 pages, submitted to TCS} } @book{gierz80, author = {G. Gierz and K. H. Hofmann and K. Keimel and J. D. Lawson and M. Mislove and D. S. Scott}, title = {A Compendium of Continuous Lattices}, publisher = {Springer Verlag}, year = {1980} } @book{gierz03, author = {G. Gierz and K. H. Hofmann and K. Keimel and J. D. Lawson and M. Mislove and D. S. Scott}, title = {Continuous Lattices and Domains}, publisher = {Cambridge University Press}, series = {Encyclopedia of Mathematics and its Applications}, volume = 93, year = {2003}, note = {Revised and expanded edition of \cite{gierz80}} } @Unpublished{keimel03, author = {Keimel, K. and Lawson, J. D.}, title = {Measure extension theorems for $T_0$-spaces}, note = {34pp, under review} } @Unpublished{keimel03a, author = {Keimel, K.}, title = {The probabilistic powerdomain for the upwards topology of a compact ordered space}, note = {13pp, under review} } @Unpublished{farjudian2003a, author = {Amin Farjudian}, title = {Sequentiality of wRPCF}, note = {Presented in the Workshop Domains VI, Birmingham, September 16--19, 2002} } @Unpublished{farjudian2003b, author = {Amin Farjudian}, title = {Conservativity of wRPCF over PCF}, note = {Presented in BCTCS 19, Leicester, England, April 7--9, 2003} } @Article{escardo04, author = {Escard\'o M. H. and Hofmann, M. and Streicher, {Th}.}, title = {On the non-sequential nature of the interval-domain model of exact real-number computation}, journal = {Mathematical Structures in Computer Science}, year = 2004, note = {Accepted for publication} } @misc{win1, author={Nygaard, M. and Winskel, G.}, title={Full abstraction for HOPLA}, note={In proc. CONCUR'03}} @misc{win2, author={Nygaard, M. and Winskel, G.}, title={Domain theory for concurrency}, note={Accepted for the Theoretical Computer Science special edition on the occasion of Dana Scott's 70th birthday, 2003}} @misc{win3, author={Varacca, D.}, title={Two denotational models for probabilistic computation }, note={PhD thesis available from \url{www.brics.dk/~varacca/}}} @misc{win4, author={E. Cheng, M. Hyland and J. Power}, title={Pseudo-distributive laws}, note={In Proceedings of Mathematical Foundations of Programming Semantics, eds. Stephen Brookes and Prakash Panangaden. Electronic Notes in Theoretic Computer Science 83, (2003), 12 pages}} @inproceedings{HMR03:tbtamcds, author = {Hennessy, Matthew and Merro, Massimo and Rathke, Julian}, title = {Towards a behavioural theory of access and mobility control in distributed systems}, year = 2003, booktitle = {Proc. FoSSaCs 2003, 6th International Conference on Foundations of Software Science and Computation Structures, Warsaw}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = 2620, pages = {282--298}, } @techreport{HRY03:slcmc, author = {Hennessy, Matthew and Rathke, Julian and Yoshida, Nobuko}, title = {SafeDpi: a language for controlling mobile code}, year = {2003}, institution = {University of Sussex}, type = {Computer Science Report}, number = {02-2003}, note = {To appear in FoSSaCS 2004} } @inproceedings{JR03:cehopcr, author = {Jeffrey, Alan and Rathke, Julian}, title = {Contextual equivalence for higher-order pi-calculus revisited}, year = {2003}, booktitle = {Proc. MFPS 2003, 19th Conference on Mathematical Foundations of Programming Semantics}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, } @InProceedings{crypto:ambients, author = {M. Bugliesi and S. Crafa and A. Prelic and V. Sassone}, title = {Secrecy in Untrusted Networks}, booktitle = {Proceedings of 30th International Colloquium on Automata, Languages and Programming, ICALP {2003}}, year = 2003, series = {LNCS}, number = 2719, pages ={969-983}, publisher = {Springer} } @InProceedings{nba, author = {M. Bugliesi and S. Crafa and M. Merro and V. Sassone}, title = {Communication Interference in Mobile Boxed Ambients}, booktitle = {Proceedings of the 22nd Conference on Foundations of Software Technology and Theoretical Computer Science}, pages = {71--84}, year = 2002, volume = 2556, series = {LNCS}, publisher = {Springer} } @Article{nba:full, author = {M. Bugliesi and S. Crafa and M. Merro and V. Sassone}, title = {Communication and Mobility Control in Boxed Ambients}, journal = {Information and Computation}, year = 2003, note = {To appear} } @InProceedings{ fmt, author = {M. Carbone and M. Nielsen and V. Sassone}, title = {A Formal Model for Trust in Dynamic Networks}, booktitle = {Proceedings of Int. Conf. on Software Engineering and Formal Methods, SEFM 2003}, pages = {54--61}, editor = {A. Cerone and P. Lindsay}, publisher = {IEEE Computer Society}, note = {A preliminary version appears as Technical Report BRICS RS-03-4, Aarhus University}, year = 2003 } @InProceedings{ boca, author = {F. Barbanera and M. Bugliesi and M. Dezani and V. Sassone}, title = {A Calculus of Bounded Capacities}, booktitle = {Proceedings of Advances in Computing Science, 9th Asian Computing Science Conference, ASIAN'03}, pages = {205--223}, year = 2003, volume = {2896}, series = {LNCS}, publisher = {Springer} } @InProceedings{dta, author = {C. Lhoussaine and V. Sassone}, title = {A Dependently Typed Ambient Calculus}, booktitle = {Proceedings of European Symposium on Programming, ESOP'03}, series = {LNCS}, publisher = {Springer}, note = {To appear} } @inproceedings{ddp:cealmp, author = "Vincent Danos and Jos{\'e}e Desharnais and Prakash Panangaden", title = "Conditional Expectations and the Approximation of Labeled {Markov} {P}rocesses", booktitle={Proceedings of CONCUR'03, Marseille, France}, publisher="Springer-Verlag", series="Lecture Notes in Computer Science", volume="2761", year= "2003", dmi-category="intc", dmi-status="", dmi-time="", x-labintel="com", } @inproceedings{dd:lmp, author = "Vincent Danos and Jos{\'e}e Desharnais", title = "Labeled {Markov} {P}rocesses: Stronger and Faster Approximations", BOOKTITLE = "Proceedings of the 18$^{th}$ Symposium on Logic in Computer Science", PUBLISHER = "IEEE Computer Society Press", ADDRESS = "Ottawa", year= "2003", dmi-category="intc", dmi-time="", x-labintel="com", } @inproceedings{DaLa02a, author = {Vincent Danos and Cosimo Laneve}, title = "Core Formal Molecular Biology", booktitle={Proceedings of the 12th European Symposium on Programming (ESOP'03, Warsaw, Poland)}, publisher="Springer-Verlag", series="Lecture Notes in Computer Science", volume="2618", pages={302--318}, month=APR, year = "2003", dmi-category="intc", dmi-status="", dmi-time="", x-labintel="com", } @misc{bod1, author={C.Bodei and P.Degano and C. Priami and N. Zannone}, title={An Enhanced CFA for Security Policies}, note={ Proceedings of the Workshop on Issues on the Theory of Security (WITS'03), (co-located with ETAPS'03), pp.131-145, Warszawa, 2003}} @misc{bod2, author={C.Bodeiand P.Degano and R.Focardi and C.Priami}, title={Authentication Primitives for Protocol Specifications}, note={ Proceedings of PaCT'03, LNCS 2763, pp. 49 - 65, Nizhny Novgorod, Russia, September 2003}} @misc{bod3, author={M. Hyland and J. Power}, title={Symmetric monoidal Sketches and categories of wirings}, note={Accepted to appear in Proceedings of CMCIM 2003. To appear in Electronic Notes in Computer Science}} @misc{bod4, title={ Passive Attack Analysis for Connection-Based Anonymity Systems}, author={Andrei Serjantov and Peter Sewell}, note={ESORICS 2003}} @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{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/}, theme = {?}, 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/}, theme = {?}, 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}, theme = {?}, 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{\'o} 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} } @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)}, } @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}, } @TechReport{BirkedalL:defp-tr, author ={L. Birkedal and R.E. M{\o}gelberg}, title ={On the Definition of Parametricity}, institution ={The IT University of Copenhagen}, year =2004, number =44, } @InProceedings{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}, } @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} } @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 } @Article{ChristensenGlueck:04:ONOFF, author={Christensen, Niels H. and Gl{\"u}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}, abstract={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} } @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} } @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.} } @InProceedings{GlueckKawabe:04:LRinv, author= {Gl{\"u}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}, abstract= {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} } @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} } @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}, pages= {101}, abstract= { 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.} } @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}, abstract= {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.} } @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}, abstract= {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 automatic (as automatic as the specialiser      is); general, in that it applies to all of the      interpreter's input programs; and      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.} } @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}, address= {Vancouver, Canada}, series= {Lecture Notes in Computer Science}, volume= {3286}, pages= {436--455}, month= {October}, abstract= {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. } } @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)}, address= {Oslo, Norway}, series= {Technical report TR-ICS-04-22, Donald Bren School of Information and Computer Science, University of California, Irvine}, pages= {1--5}, month= {June}, abstract= {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. } } @Article{lawall:scp04, author= {Charles Consel and Julia L. Lawall and Anne-Francoise Le Meur}, year= {2004}, title= {A Tour of Tempo: a Program Specializer for the C language}, journal= {Science of Computer Programming}, volume= {52}, pages= {341--370}, abstract= {  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. } } @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}, abstract={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. } } @string{lncs = "Lecture Notes in Computer Science"} @string{springer = "Springer-Verlag"} @string{acm = "ACM Press"} @string{jfp = "Journal of Functional Programming"} @string{mscs = "Mathematical Structures in Computer Science"} @InProceedings{2004-Frisch-Cardelli-icalp, 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, 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} } @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{\'e}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 = {{\'E}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 } @MastersThesis{2004-Yakobowski-DEA, author = {Boris Yakobowski}, title = {{\'E}tude s{\'e}mantique d'un langage interm{\'e}diaire de type Static Single Assignment}, school = {ENS Cachan}, year = {2004}, month = sep, } @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{\~n}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}, 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{\'e}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}} @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{\'e}vy}, MONTH = {Aug}, ORGANIZATION = {Jean-Jacques L{\'e}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 = {} } @INPROCEEDINGS{cansell04a, CRINNUMBER = {A04-R-091}, CATEGORY = {3}, EQUIPE = {MOSEL}, AUTHOR = {Cansell, Dominique and Culat, Jean-Fran\c{c}ois and M{\'e}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 Specification incrementale du systeme}, 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 Mery, 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{\^u}re de syst{\`e}mes {\'e}lectroniques}, JOURNAL = {G{\'e}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}, } @INPROCEEDINGS{bournez04i, CRINNUMBER = {A04-R-419}, CATEGORY = {3}, EQUIPE = {PROTHEO}, AUTHOR = {Bournez, Olivier and Cucker, Felipe and Jacob{\'e} 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{\'e}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{\'e}}, 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{\'e} 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, AUTHOR = {Bournez, Olivier and Cucker, Felipe and Jacob{\'e} 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}, 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{\'e} 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{\'e} 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. }, } @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}, 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}} } @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}, 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.}, } @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, 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}, year = {2004}, pages = {494-505}, url = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3142{\&}spage=494} } @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} @InProceedings{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} } @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}, url={http://danae.uni-muenster.de/lehre/kuchen/JFLP/} } @InProceedings{Danvy:CW04, 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{\"a}t zu Kiel, Institut f{\"u}r Informatik und Praktische Mathematik}, address = {L{\"u}beck, Germany} } @InProceedings{Danvy:WRS04, 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} } @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. } } @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. } } @InProceedings{Cal+Mog+Tah:ESOP-2004, author = {C. Calcagno and E. Moggi and W. Taha}, title = {{ML}-like Inference for Classifiers}, 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. } } @InProceedings{GPCE2004, title={Generative Programming and Component Engineering}, booktitle ={Generative Programming and Component Engineering}, series =LNCS, publisher =SV, volume =3286, month =Oct, year =2004, address ={Vancouver}, editor ={G. Karsai  and E. Visser} } @InProceedings{ESOP2004, title =ESOP2004, booktitle =ESOP2004, key ={ES{\relax OP} '04}, year =2004, series =LNCS, volume =2986, publisher =SV, date ={2004-03-29/--04-02}, publisher ={Springer-Verlag Berlin and Heidelberg GmbH & Co. KG}, address ={Barcelona, Spain}, note ={held as part of ETAPS 2004}, editor ={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} } @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} } @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} } @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} } @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" } @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 } @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 } @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.} } @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.}, url= {http://www.di.unito.it/~paolini/papers/cometa5.pdf}, publisher={Elsevier} } @inproceedings{Dennis:disproving04, 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, 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, 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, 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, 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, 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, author ="Graham Hutton", title ="{Programming in Haskell}", note ="In preparation", year =2004 } @inproceedings{atannasow:jeuring:mpc04, 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, 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, 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, author ={Andres L\"oh}, title ={Exploring Generic Haskell}, school ={Utrecht University}, year =2004 } @inproceedings{ambler-crole-momigiliano, 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, 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, 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, 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, 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, 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}, year ={2004} } @article{ghani-tia04, 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{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"} @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} } @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}, }        @UNPUBLISHED{DawGarGhe-complexity, author="A. Dawar and P. Gardner and G. Ghelli", title="Expressiveness and Complexity of Graph Logic", note="In preparation" } @INPROCEEDINGS{DawGarGhe04lrpp, author="A.Dawar and P. Gardner and G. Ghelli", title = "Adjunct Elimination Through Games", booktitle = "Proc.\ LRPP, Turku, Finland", year = 2004, } @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.\ of the 24th FSTTCS, Chennai, India", month = "December", Year = 2004 } @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 } @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 = "Dodicesimo Convegno su Sistemi Evoluti per Basi di Dati (SEBD), S.Margherita di Pula, Cagliari, Italy", pages = "394--401", year = 2004 } @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 } @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}, } @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} } @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", note= "{\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", note= "{\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. {\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). {\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", note= "{\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", note= "{\bf APPSEM Themes G,H}", year = "2005" } @inproceedings{GW04, author = "P. Gardner and S. Maffeis", title = "Behavioural Equivalences for Dynamic Web Data", note= "{\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", note= "{\bf APPSEM Theme H}", year = "2004" } @Book{Ritter:sembook, author = {D. J. Pym and E. Ritter}, title = {Reductive Logic and Proof-search: Proof Theory, Semantics, and Control}, publisher = {Oxford University Press}, year = 2004, number = 45, series = {Oxford Logic Guide}, theme = {DF}, workpackage = {12}, site = {Birmingham} } @techreport{cw04, author = {Hayo Thielecke (ed.)}, title = {Proceedings of the Fourth {ACM} {SIGPLAN} Continuations Workshop {(CW'04)}}, number = {CSR-04-1}, institution = {School of Computer Science, University of Birmingham}, address = {Birmingham B15 2TT, United Kingdom}, year = 2004, theme = {E}, workpackage = {2}, site = {Birmingham} } @inproceedings{answertypecbn, author = {Hayo Thielecke}, title = {Answer Type Polymorphism in Call-by-name Continuation Passing}, booktitle = {European Symposium on Programming (ESOP 2004)}, publisher = {Springer}, series = {{LNCS}}, volume = {2986}, year = 2004, pages = {279--293}, theme = {E}, workpackage = {}, site = {Birmingham} } @Article{cpssemantics, author = {Carsten F\"uhrmann and Hayo Thielecke}, title = {On the call-by-value {CPS} transform and its semantics}, journal = {Information and Computation}, year = 2004, number = 2, volume = {188}, pages = {241--283}, theme = {E}, workpackage = {}, site = {Birmingham} } @Techreport{ReusSchwing, Author = "Bernhard Reus and Jan Schwinghammer", Title = " Denotational Semantics for {A}badi and {L}eino's Logic of Objects", Institution = " University of Sussex", Note = "Submitted", number = "03/04", Year = 2004, theme = {D}, workpackage = {}, site = {Sussex} } @article{ReusStreicher:TCS:04, author = {B.~Reus and Th.~Streicher}, title = "{Semantics and logic of object calculi}", journal = {TCS}, volume = 316, year = 2004, pages = {191-213} } @Article{HNR04journal, title={SafeDpi: A Language for Controlling Mobile Code}, author={Matthew Hennessy and Julian Rathke and Nobuko Yoshida}, journal={Acta Informatica}, year=2005, note={To appear}, theme = {G}, workpackage = {}, site = {Sussex} } @InProceedings{HNR04, title={SafeDpi: A Language for Controlling Mobile Code (extended abstract)}, author={Matthew Hennessy and Julian Rathke and Nobuko Yoshida }, booktitle={Conference Record of FOSSACS04}, year=2004, series={Lecture notes in Computer Science}, volume={2987}, pages={241-256}, isbn={3-540-21298-1}, theme = {G}, workpackage = {}, site = {Sussex} } @InProceedings{GHS:FGUC04, author = {D. Gorla and M. Hennessy and V. Sassone}, title = {Security Policies as Membranes in Systems for Global Computing}, editor = {J. Rathke}, booktitle = {Proc. of 3rd EATCS Workshop on Foundations of Global Ubiquitous Computing (FGUC'04)}, series = {ENTCS}, volume = {}, pages = {}, year = {2004}, publisher = {Elsevier}, theme = {G}, workpackage = {}, site = {Sussex} } @TECHREPORT{CMS04, AUTHOR = "R. Chadha and D. Macedonio and V. Sassone", TITLE = "A Distributed Kripke Semantics", INSTITUTION = "University of Sussex", YEAR = "2004", note = "To appear", theme = {G}, workpackage = {}, site = {Sussex} } @Article{bun ,author = {V. Sassone and P. Sobociski} ,title = {Locating Reaction with 2-categories} ,journal = {Theoretical Computer Science} ,year = {2004} ,volume = "xx" ,number = "yy" ,pages = "xx--xx" ,note = "To appear. Extends and improves a paper appeared in Fossacs'03" ,theme = {G} ,workpackage = {} ,site = {Sussex} } @Article{BugCraMerSas:NBA:0X ,author = "Bugliesi, M. and Crafa, S. and Merro, M. and Sassone, V." ,title = "{Communication and Mobility Control in Boxed Ambients}" ,journal = "Information and Computation" ,year = "200X" ,volume = "xx" ,number = "xx" ,pages = "xx -- xx" ,note = "To appear. Extends and improves a paper appeared in=20 FST=EF=BF=BDTCS'02" ,theme = {G} ,workpackage = {} ,site = {Sussex} } @InProceedings{LhoSas:ESOP:04 ,author = {C. Lhoussaine and V. Sassone} ,title = {A Dependently Typed Ambient Calculus} ,booktitle = {Proceedings of European Symposium on Programming,=20 ESOP'04} ,pages = {171-187} ,year = 2004 ,volume = 2986 ,series = {Lecture Notes in Computer Science} ,publisher = {Springer-Verlag} ,theme = {G} ,workpackage = {} ,site = {Sussex} } @inproceedings{CC04, author = "J. Laird", title = "A Calculus of Coroutines", booktitle = "Proceedings of ICALP '04", pages = "882--893", publisher = "Springer-Verlag", series = "LNCS", number = 3142, note = "Extended version submitted to special issue of Theoretical Computer Science", year = 2004 ,theme = {F} ,workpackage = {} ,site = {Sussex} } @InProceedings{Marcial:Escardo04, author = {Marcial-Romero, J.R. and Escard\'o, M.H.}, title = {Semantics of a Sequential Language for exact real-number computation}, booktitle = {Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science}, pages = {426--435}, year = {2004}, month = {July}, publisher = {IEEE Computer Society}, theme = {DFI}, workpackage = {}, site = {Birmingham} } @Article{escardo:synthetic, author = {M.H. Escard\'o}, title = {Synthetic topology of data types and classical spaces}, journal = {Electron. Notes Theor. Comput. Sci.}, year = 2004, volume = 87, issue = {C}, pages = {21--156}, theme = {DFI}, workpackage = {}, site = {Birmingham} } @ARTICLE{PPExp, AUTHOR={Vickers, S.J.}, TITLE={The Double Powerlocale and Exponentiation: A Case Study in Geometric Reasoning}, JOURNAL={Theory and Applications of Categories}, VOLUME=12, YEAR=2004, PAGES={372--422}, THEME={I}, WORKPACKAGE={}, SITE={Birmingham} } @ARTICLE{EntSys, AUTHOR={Vickers, Steven}, TITLE={Entailment Systems for Stably Locally Compact Locales}, JOURNAL={Theoretical Computer Science}, ISSN={0304-3975}, VOLUME=316, PAGES={259--296}, YEAR=2004, THEME={I}, WORKPACKAGE={}, SITE={Birmingham} } @ARTICLE{UniCharPP, AUTHOR={Vickers, S.J. and Townsend, C.F.}, TITLE={A Universal Characterization of the Double Powerlocale}, JOURNAL={Theoretical Computer Science}, ISSN={0304-3975}, VOLUME=316, YEAR=2004, PAGES={297--321}, THEME={I}, WORKPACKAGE={}, SITE={Birmingham} } @INPROCEEDINGS{HillVickers:LangCMLS, AUTHOR={Hill, Gillian and Vickers, Steven}, TITLE={A Language for Configuring Multi-Level Specifications}, EDITOR={Rattray, Charles and Maharaj, Savitri and Shankland, Carron}, BOOKTITLE={Algebraic Methodology and Software Technology, 10th International Conference, AMAST 2004, Stirling, Scotland}, PUBLISHER={Springer-Verlag}, SERIES={Lecture Notes in Computer Science}, NUMBER=3116, YEAR=2004, ISBN={3-540-22381-9}, PAGES={196--210}, THEME={D}, WORKPACKAGE={}, SITE={Birmingham} } @UNPUBLISHED{ConstrTychonoff, AUTHOR={Vickers, Steven}, TITLE={Some Constructive Roads to {T}ychonoff}, YEAR=2004, NOTE={accepted for publication in Proceedings of ``From Sets and Types to Topology and Analysis: Practicable Foundations for Constructive Mathematics'', Venice 2003}, THEME={I}, WORKPACKAGE={}, SITE={Birmingham} } @UNPUBLISHED{CompLocFT, AUTHOR={Vickers, Steven}, TITLE={Compactness in Locales and Formal Topology}, YEAR=2002, NOTE={submitted for publication, draft available on web at \texttt{http://www.cs.bham.ac.uk/\~{}sjv}}, THEME={I}, WORKPACKAGE={}, SITE={Birmingham} } @UNPUBLISHED{LocCompA, AUTHOR={Vickers, Steven}, TITLE={Localic Completion of Generalized Metric SPaces {I}}, YEAR=2003, NOTE={submitted for publication, draft available on web at \texttt{http://www.cs.bham.ac.uk/\~{}sjv}}, THEME={I}, WORKPACKAGE={}, SITE={Birmingham} } @UNPUBLISHED{LocCompB, AUTHOR={Vickers, Steven}, TITLE={Localic Completion of Generalized Metric Spaces {I}{I}: Powerlocales}, YEAR=2003, NOTE={draft available on web at \texttt{http://www.cs.bham.ac.uk/\~{}sjv}}, THEME={I}, WORKPACKAGE={}, SITE={Birmingham} } @InProceedings{HylandLevyPlotkinPower:combinecont, author = {J. M. E. Hyland and P. B. Levy and G. D. Plotkin and A. J. Power}, title = {Combining continuations with other effects}, booktitle = {Proc., 4th ACM-SIGPLAN Workshop on Continuations}, year = 2004, theme = {E}, workpackage = {}, site = {Birmingham} } @Unpublished{Levy:inftraceno, author = {P. B. Levy}, title = {Infinite trace semantics}, note = {Proceedings of the 2nd APPSEM II Workshop, Tallinn, Estonia, \texttt{www.cs.ioc.ee/appsem04/accepted.html}}, month = {April}, year = 2004, theme = {G}, workpackage = {}, site = {Birmingham} } @Book{Levy:thesisbook, author = {P. B. Levy}, title = {Call-By-Push-Value}, publisher = {Kluwer}, year = 2004, series = {Semantic Structures in Computation}, month = {March}, note = {}, theme = {DEF}, workpackage = {}, site = {Birmingham} } @Unpublished{Levy:adjunctionsjourn, author = {P. B. Levy}, title = {Adjunction Models For Call-By-Push-Value With Stacks}, note = {to appear in Theory and Applications of Categories}, theme = {EF}, workpackage = {}, site = {Birmingham} } @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.}, theme = {I}, workpackage = {}, site = {Birmingham} } @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, theme = {EF}, workpackage = {}, site = {Birmingham} } @Article{RS04, author ={B. Reus and T. Streicher}, title ={\it Semantics of Object Calculi}, journal ={TCS 316, no.1--3}, pages ={191--213.}, year ={2004}} @Article{K04, author ={K. Keimel}, title ={\it The Probabilistic Powerdomain for Stably Compact Spaces via Compact Ordered Spaces}, journal ={ENTCS vol.~87, }, pages ={225--238.}, year = {2004}} @Article{KL04, author ={K. Keimel and J.H. Liang}, title ={\it Order environments of topological spaces}, journal ={Acta Mathematica Sinica 20}, pages ={943--948.}, year ={2004}} @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} } @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{\~a}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{\~a}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 Point-free Calculus Less Pointless", author = "A.~Cunha and J.~S. Pinto", booktitle = "Proc of the 2nd APPSEM II Workshop", pages = "178--179", year = 2004 } @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 } @UNPUBLISHED{AMU:itecsh, AUTHOR = "Andreas Abel and Ralph Matthes and Tarmo Uustalu", TITLE = "Iteration and Coiteration Schemes for Higher-Order Nested Datatypes", NOTE = "To appear in Theor.\ Comput.\ Sci., special issue FoSSaCS'03", MONTH = jul, YEAR = 2004 } @ARTICLE{MU:subnsv, AUTHOR = "Ralph Matthes and Tarmo Uustalu", TITLE = "Substitution in Non-Wellfounded Syntax with Variable Binding", JOURNAL = "Theor.\ Comput.\ Sci.", VOLUME = 327, NUMBER = "1--2", SPECIAL = "Selected Papers from 6th Int.\ Wksh.\ on Coalgebraic Methods in Computer Science, CMCS '03 (Warsaw, Poland, 5--6 Apr.\ 2003)", PAGES = "155--174", YEAR = 2004 } @ARTICLE{GU:copim, AUTHOR = "Neil Ghani and Tarmo Uustalu", TITLE = "Coproducts of Ideal Monads", JOURNAL = "Theor.\ Inform.\ and Appl.", VOLUME = 38, NUMBER = 4, PAGES = "321--342", YEAR = 2004 } @INCOLLECTION{AU:norel2, AUTHOR = "Thorsten Altenkirch and Tarmo Uustlau", TITLE = "Normalization by Evaluation for $\lambda^{\to,2}$", EDITOR = "Yukiyoshi Kameyama and Peter J. Stuckey", BOOKTITLE = "Proc.\ of 7th Int.\ Symp.\ on Functional and Logic Programming, FLOPS 2004 (Nara, Japan, 7--9 Apr. 2004)", SERIES = "Lect.\ Notes in Comput.\ Sci", VOLUME = 2998, PAGES = "260--275", PUBLISHER = "Springer-Verlag", ADDRESS = "Berlin", YEAR = 2004 } @INCOLLECTION{CUV:reccc, AUTHOR = "Venanzio Capretta and Tarmo Uustalu and Varmo Vene", TITLE = "Recursive Coalgebras from Comonads", EDITOR = "J{\'{\i}}{\v{r}}i Ad{\'a}mek and Stefan Milius", BOOKTITLE = "Proc.\ of 7th Int.\ Wksh.\ on Coalgebraic Methods in Computer Science, CMCS 2004 (Barcelona, Spain, 29--31 March 2004)", SERIES = "Electr.\ Notes in Theor.\ Comput.\ Sci.", VOLUME = "106C", PAGES = "43--61", PUBLISHER = "Elsevier", ADDRESS= "Amsterdam", YEAR = 2004 } @INCOLLECTION{GUV:buiadu, AUTHOR = "Neil Ghani and Tarmo Uustalu and Varmo Vene", TITLE = "Build, Augment and Destroy, Universally", EDITOR = "Wei-Ngan Chin", BOOKTITLE = "Proc.\ of 2nd Asian Symp.\ on Programming Languages and Systems, APLAS 2004 (Taipei, Taiwan, 4--6 Nov. 2004)", SERIES = "Lect.\ Notes in Comput.\ Sci.", VOLUME = 3302, PAGES = "327--347", PUBLISHER = "Springer-Verlag", ADDRESS = "Berlin", YEAR = 2004 } @INCOLLECTION{GUV:genac, AUTHOR = "Neil Ghani and Tarmo Uustalu and Varmo Vene", TITLE = "Generalizing the Augment Combinator", EDITOR = "Hans-Wolfgang Loidl", BOOKTITLE = "Proc.\ of 5th Int.\ Symp.\ on Trends in Functional Programming, TFP'04 (Munich, Germany, 25--26 Nov.\ 2004)", PAGES = "65--76", PUBLISHER = "Inst.\ f\"ur Informatik, Ludwig-Maximilians-Univ.\ M\"unchen", YEAR = 2004 } @INCOLLECTION{Lau:encaac, AUTHOR = "Peeter Laud", TITLE = "Encryption in Automatic Analysies for Confidentiality against Active Adversaries", BOOKTITLE = "Proc.\ of 2004 IEEE Symp.\ on Security and Privacy, S&P 2004 (Berkeley, CA, USA, May 2004)", PAGES = "71--85", PUBLISHER = "IEEE CS Press", ADDRESS = "Los Alamitos, CA", YEAR = 2004 }