papers.bib

@INPROCEEDINGS{alti:tlca03,
  AUTHOR = {Michael Abbott and Thorsten Altenkirch and Neil Ghani 
                  and Conor McBride},
  TITLE = {Derivatives of Containers},
  BOOKTITLE = {{Typed Lambda Calculi and Applications (TLCA03)}},
  PAGES = {16--30},
  SERIES = {LNCS~2701},
  YEAR = {2003},
  URL = {http://www.cs.nott.ac.uk/~txa/publ/tlca03.pdf}
}

@ARTICLE{AlvJunKei04,
  AUTHOR = {Mauricio Alvarez-Manilla and Achim Jung and Klaus Keimel},
  TITLE = {The Probabilistic Powerdomain for Stably Compact
		 Spaces},
  JOURNAL = {TCS: Theoretical Computer Science},
  VOLUME = {328},
  NUMBER = {3},
  PAGES = {221--244},
  YEAR = {2004},
  URL = {http://www.cs.bham.ac.uk/~axj/pub/papers/measures.pdf},
  OPTURL = {http://www.sciencedirect.com/science?_ob=MImg&_imagekey=B6V1G-4CXKM12-1-1&_cdi=5674&_user=10&_orig=browse&_coverDate=12%2F03%2F2004&_sk=996719996&view=c&wchp=dGLbVzb-zSkWA&md5=20eb356b887c5984d3e3105a1d5e20b6&ie=/sdarticle.pdf},
  OPTABSTRACTURL = {http://www.sciencedirect.com/science?_ob=ArticleURL&_udi=B6V1G-4CXKM12-1&_user=10&_handle=V-WA-A-W-D-MsSAYWW-UUA-U-AAZAEZEZUV-AACECCUVUV-ACYWDABUB-D-U&_fmt=summary&_coverDate=12%2F03%2F2004&_rdoc=1&_orig=browse&_srch=%23toc%235674%232004%23996719996%23529320!&_cdi=5674&view=c&_acct=C000050221&_version=1&_urlVersion=0&_userid=10&md5=c0ec2793ae2e5049a5aa1d7c01c81c5f}
}

@INPROCEEDINGS{conf/sefm/CarboneNS03,
  TITLE = {A Formal Model for Trust in Dynamic Networks},
  AUTHOR = {Marco Carbone and Mogens Nielsen and Vladimiro
		 Sassone},
  PUBLISHER = {IEEE Computer Society},
  YEAR = {2003},
  BIBDATE = {2003-10-09},
  BIBSOURCE = {DBLP,
		 http://dblp.uni-trier.de/db/conf/sefm/sefm2003.html#CarboneNS03},
  BOOKTITLE = {Intl. Conf. on Software Engineering and Formal Methods (SEFM03)},
  OPTCROSSREF = {conf/sefm/2003},
  ISBN = {0-7695-1949-0},
  PAGES = {54--61},
  OPTURL = {http://csdl.computer.org/comp/proceedings/sefm/2003/1949/00/19490054abs.htm},
  URL = {http://eprints.ecs.soton.ac.uk/12294/01/fmtSEFMoff.pdf}
}

@INPROCEEDINGS{Cardelli,
  AUTHOR = {L. Cardelli and P. Gardner and G. Ghelli},
  TITLE = {{Manipulating Trees with Hidden Labels}},
  BOOKTITLE = {{Intl Conf on Foundations of Software Science and Computation Structures (FOSSACS03)}},
  SERIES = {LNCS~2620},
  PAGES = {216--232},
  YEAR = 2003,
  ADDRESS = {Warsaw, Poland},
  MONTH = APR,
  URL = {http://www.doc.ic.ac.uk/~pg/papers/hide.pdf}
}

@INPROCEEDINGS{edalat,
  AUTHOR = {Abbas Edalat and Dirk Pattinson},
  TITLE = {Initial value problems in domain theory},
  BOOKTITLE = {Computability and Complexity in Analysis (CCA03)},
  EDITOR = {Vasco Brattka and Matthias Schr{\"{o}}der and Klaus
		 Weihrauch and Ning Zhong},
  YEAR = {2003},
  MONTH = AUG,
  SERIES = {Informatik Berichte},
  VOLUME = {302},
  PAGES = {211--227},
  PUBLISHER = {FernUniversit{\"a}t in Hagen},
  NOTE = {International Conference, CCA 2003, Cincinnati, USA,
		 August 28--30, 2003}
}

@INPROCEEDINGS{HenRatYos04,
  AUTHOR = {Matthew Hennessy and Julian Rathke and Nobuko Yoshida},
  TITLE = {{safeDpi}: {A} Language for Controlling Mobile Code},
  BOOKTITLE = {FOSSACS: International Conference on Foundations of
		 Software Science and Computation Structures},
  SERIES = {LNCS~2620},
  PUBLISHER = {Springer},
  YEAR = {2004},
  URL = {http://www.cogs.susx.ac.uk/users/julianr/slcmc.pdf}
}

@ARTICLE{escardo04,
  AUTHOR = {M. H. Escard{\'o} and M. Hofmann and Th. Streicher},
  TITLE = {{On the non-sequential nature of the interval-domain model of real-number computation}},
  JOURNAL = {Mathematical Structures in Computer Science},
  YEAR = 2004,
  VOLUME = 14,
  NUMBER = 6,
  PAGES = {803--814},
  URL = {http://www.mathematik.tu-darmstadt.de/~streicher/ehs.ps.gz}
}

@INPROCEEDINGS{altenkirch04:_repres_nested_induc_types_w,
  AUTHOR = {T. Altenkirch and M. Abbot and N. Ghani},
  TITLE = {{Representing Nested Inductive Types using W-types}},
  BOOKTITLE = {{International Colloquium on Automata, Languages and Programming (ICALP 2004)}},
  PAGES = {59--71},
  YEAR = 2004,
  SERIES = {LNCS~3142},
  ADDRESS = {Turku, Finland, July 12--16},
  PUBLISHER = {Springer},
  URL = {http://www.cs.nott.ac.uk/~txa/publ/icalp04.pdf}
}

@ARTICLE{barthe04:_type,
  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},
  URL = {http://www.cs.ioc.ee/~tarmo/papers/mscs.ps.gz}
}

@INPROCEEDINGS{alti:flops04,
  THEME = {BE},
  SITE = {nottingham},
  AUTHOR = {Thorsten Altenkirch and Tarmo Uustalu},
  TITLE = {{Normalization by Evaluation for $\lambda^{\to 2}$}},
  BOOKTITLE = {Functional and Logic Programming (FLOPS04)},
  ISBN = {3-540-21402-X},
  YEAR = {2004},
  OPTNUMBER = {2998},
  SERIES = {LNCS~2998},
  PUBLISHER = {Springer},
  PAGES = {260--275},
  URL = {http://www.cs.nott.ac.uk/~txa/publ/flops04.pdf}
}

@INPROCEEDINGS{ghani04:_build_augmen_destr,
  AUTHOR = {Neil Ghani and Tarmo Uustalu and Varmo Vene},
  TITLE = {{Build, Augment, Destroy. Universally}},
  BOOKTITLE = {{Proceedings of Programming Languages and Systems: Second Asian Symposium, (APLAS04)}},
  PAGES = {327--341},
  YEAR = 2004,
  SERIES = {LNCS~3302},
  PUBLISHER = {Springer},
  URL = {http://www.cs.ioc.ee/~tarmo/papers/aplas04.pdf}
}

@ARTICLE{ghani04:_coprod_ideal_monad,
  AUTHOR = {Neil Ghani and Tarmo Uustalu},
  TITLE = {{Coproducts of Ideal Monads}},
  JOURNAL = {{Journal of Theoretical Informatics and Applications}},
  YEAR = 2004,
  VOLUME = 38,
  PAGES = {321--342},
  URL = {http://www.cs.ioc.ee/~tarmo/papers/fics03-tia.ps.gz}
}

@ARTICLE{abel05:_iterat,
  AUTHOR = {Andreas Abel and Ralph Matthes and Tarmo Uustalu},
  TITLE = {Iteration and coiteration schemes for higher-order and nested datatypes},
  JOURNAL = {{Theoretical Computer Science}},
  YEAR = 2005,
  VOLUME = 33,
  NUMBER = {1--2},
  PAGES = {327--341},
  NOTE = {FOSSACS special issue},
  URL = {http://www.tcs.informatik.uni-muenchen.de/~abel/tcs04.pdf}
}

@INPROCEEDINGS{conforti04:_decid,
  AUTHOR = {G. Conforti and G. Ghelli},
  TITLE = {{Decidability of freshness, undecidability of revelation}},
  BOOKTITLE = {{Proc. of Foundations of Software Science and Computation Structures (FOSSACS04)}},
  PAGES = {105--120},
  YEAR = 2004,
  SERIES = {LNCS~2987},
  ADDRESS = {Barcelona, Spain},
  MONTH = MAR,
  PUBLISHER = {Springer},
  URL = {http://springerlink.com/content/ka96pa461awylhxx/fulltext.pdf}
}

@INPROCEEDINGS{conforti04:_xml_p2p,
  AUTHOR = {G. Conforti and G. Ghelli and P. Manghi and C. Sartiani},
  TITLE = {{A self-organizing XML  P2P database system}},
  BOOKTITLE = {{Proc. of Dodicesimo Convegno su Sistemi Evoluti per Basi di Dati (SEBD)}},
  PAGES = {394--401},
  YEAR = 2004,
  SERIES = {LNCS~3268},
  ADDRESS = {Cagliari, Italy},
  PUBLISHER = {Springer},
  URL = {http://www.di.unipi.it/~ghelli/papers/SarManGhe04-p2pdb.pdf}
}

@INPROCEEDINGS{bornat05:_permis,
  AUTHOR = {Richard Bornat and Cristiano Calcagno and Peter {O'Hearn} and Matthew Parkinson},
  TITLE = {Permission accounting in separation logic},
  NOTE = {ACM SIG{\-}PLAN Notices 40(1)},
  OPTVOLUME = 40,
  OPTNUMBER = 1,
  PAGES = {259--270},
  MONTH = JAN,
  BOOKTITLE = {{Proceedings of POPL 2005: The 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}},
  YEAR = 2005,
  ADDRESS = {Long Beach, CA},
  URL = {http://www.doc.ic.ac.uk/~ccris/ftp/permissions\_paper.pdf}
}

@INPROCEEDINGS{parkinson05:_separ,
  AUTHOR = {Matthew Parkinson and Gavin Biermann},
  TITLE = {Separation logic and abstraction},
  NOTE = {ACM SIG{\-}PLAN Notices 40(1)},
  OPTVOLUME = 40,
  OPTNUMBER = 1,
  PAGES = {247--258},
  MONTH = JAN,
  BOOKTITLE = {{Proceedings of POPL 2005: The 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}},
  YEAR = 2005,
  ADDRESS = {Long Beach, CA},
  URL = {http://www.appsem.org/papers/parkinson.pdf}
}

@MISC{rosolini04:_using_synth_domain_theor,
  AUTHOR = {G. Rosolini and A. Simpson},
  TITLE = {{Using Synthetic Domain Theory to prove operational properties of a powerful polymorphic language}},
  YEAR = 2004,
  MONTH = FEB,
  URL = {http://homepages.inf.ed.ac.uk/als/Research/usdt.pdf}
}

@TECHREPORT{birkedal04:_categ,
  AUTHOR = {L. Birkedal and G. Rosolini},
  TITLE = {Categories of reflexive graphs},
  INSTITUTION = {The IT University of Copenhagen},
  YEAR = 2004
}

@TECHREPORT{hyland04:_remar,
  AUTHOR = {J.M.E. Hyland and M. Nagayama and G. Rosolini},
  TITLE = {Remarks on the finite-powerset functor on relations},
  INSTITUTION = {Univ of Cambridge},
  YEAR = 2004
}

@ARTICLE{birkedal04:_recen_devel_domain_theor,
  AUTHOR = {L. Birkedal and M. Escardo and A. Jung and G. Rosolini},
  TITLE = {{Recent Developments in Domain Theory}},
  JOURNAL = {Theoretical Computer Science},
  YEAR = 2004,
  VOLUME = 316,
  NUMBER = {1--3}
}

@INPROCEEDINGS{visser04:_tutor,
  AUTHOR = {Joost Visser and Joao Saraiva},
  TITLE = {{Tutorial on strategic programming across paradigms}},
  BOOKTITLE = {{Proc. 8th Brazilian Symposium on Programming Languages}},
  YEAR = 2004,
  ADDRESS = {Niteroi, Brasil}
}

@TECHREPORT{edalat03:_initial,
  AUTHOR = {A. Edalat and D. Pattinson},
  TITLE = {{Initial value problems in domain theory}},
  INSTITUTION = {Dept of Computing},
  ADDRESS = {Imperial College, London},
  OPTBOOKTITLE = {Proccedings of CCA 03},
  YEAR = 2003
}

@INPROCEEDINGS{edalat03,
  AUTHOR = {Abbas Edalat and Dirk Pattinson},
  TITLE = {A domain theoretic account of picard's theorem},
  BOOKTITLE = {{International Colloquium on Automata, Languages and Programming (ICALP03)}},
  YEAR = 2003,
  URL = {http://www.doc.ic.ac.uk/~ae/papers/picard.siam5.ps}
}

@INPROCEEDINGS{edalat03:initial,
  AUTHOR = {A. Edalat and D. Pattinson},
  TITLE = {{Initial value problems in domain theory}},
  BOOKTITLE = {{Proceedings of Computability and Complexity in Analysis (CCA03)}},
  YEAR = 2003,
  URL = {http://www.appsem.org/papers/initial-value-problems-in.ps}
}

@INPROCEEDINGS{benton04:_shrin_sml,
  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 (IFL04)}},
  PAGES = {142--159},
  YEAR = 2004,
  SERIES = {LNCS~3474},
  PUBLISHER = {Springer},
  URL = {http://www.dcs.ed.ac.uk/home/samuel/Papers/shrinking.pdf}
}

@ARTICLE{Filinski-Rohde:RAIRO05,
  AUTHOR = {Andrzej Filinski and Henning Korsholm Rohde},
  TITLE = {Denotational Aspects of Untyped Normalization by Evaluation},
  JOURNAL = {Theoretical Informatics and Applications},
  YEAR = 2005,
  VOLUME = 39,
  NUMBER = 3,
  PAGES = {423-453},
  THEME = {C},
  SITE = {Copenhagen and Aarhus},
  URL = {http://www.diku.dk/hjemmesider/ansatte/andrzej/papers/DAoUNbE.pdf}
}

@ARTICLE{coquand+:lf-dependently-records,
  AUTHOR = {Thierry Coquand and Randy Pollack and Makoto Takeyama},
  TITLE = {{A Logical Framework with Dependently Typed Records}},
  PAGES = {112--134},
  JOURNAL = {Fundamenta Informaticae},
  YEAR = 2005,
  VOLUME = 65,
  NUMBER = {1--2},
  URL = {http://www.dcs.ed.ac.uk/home/rap/export/TLCA03extended.ps.gz}
}

@ARTICLE{CarGheGor05-ic,
  AUTHOR = {L. Cardelli and G. Ghelli and A. D. Gordon},
  TITLE = {Secrecy and Group Creation},
  JOURNAL = {Information and Computation},
  YEAR = 2005,
  MONTH = {Jan},
  VOLUME = {196},
  NUMBER = {2},
  PAGES = {127--155},
  OPTNOTE = {To appear},
  THEME = {G},
  SITE = {pisa,microsoft},
  URL = {http://www.appsem.org/papers/SecrecyandGroupCreation.pdf}
}

@INCOLLECTION{aspinall/hofmann:dependent-types,
  AUTHOR = {David Aspinall and Martin Hofmann},
  TITLE = {Dependent Types},
  BOOKTITLE = {Advanced Topics in Types and Programming Languages},
  PAGES = {45--86},
  PUBLISHER = {MIT press},
  YEAR = 2005,
  EDITOR = {Benjamin Pierce},
  CHAPTER = 2,
  URL = {http://homepages.inf.ed.ac.uk/da/papers/attapl/}
}

@ARTICLE{tkp:05,
  JOURNAL = {{Electronic Notes in Theoretical Computer Science}},
  VOLUME = 129,
  TITLE = {Semantic Domains for Combining Probability and Non-Determinism},
  AUTHOR = {Tix, Regina and Keimel, Klaus and Plotkin, Gordon D.},
  YEAR = 2005,
  PAGES = {1--104},
  URL = {http://www.appsem.org/papers/Tix_semdom.pdf}
}

@INCOLLECTION{GUV:genac,
  AUTHOR = {Neil Ghani and Tarmo Uustalu and Varmo Vene},
  TITLE = {Generalizing the {augment} Combinator},
  EDITOR = {Hans-Wolfgang Loidl},
  BOOKTITLE = {Trends in Functional Programming 5},
  PAGES = {65--78},
  PUBLISHER = {Intellect},
  YEAR = 2006,
  URL = {http://www.cs.ioc.ee/~tarmo/papers/tfp04-book.pdf}
}

@INPROCEEDINGS{urban/cheney:avoiding-equivariance,
  AUTHOR = {Christian Urban and James Cheney},
  TITLE = {{Avoiding Equivariance in Alpha-Prolog}},
  BOOKTITLE = {Typed Lambda Calculi and Applications: Proceedings of the
                  Seventh International Conference TLCA~2005},
  PAGES = {401--416},
  YEAR = 2005,
  SERIES = {LNCS~3461},
  OPTSERIES = {Lecture Notes in Computer Science},
  PUBLISHER = {Springer-Verlag},
  OPTURL = {http://dx.doi.org/10.1007/11417170_29},
  URL = {http://www4.in.tum.de/~urbanc/Publications/alpha-tlca.ps}
}

@INPROCEEDINGS{aspinall+:mrg-smart-devices,
  AUTHOR = {David Aspinall and Stephen Gilmore and Martin
                  Hofmann and Donald Sannella and Ian Stark},
  TITLE = {Mobile Resource Guarantees for Smart Devices},
  BOOKTITLE = {Construction and Analysis of Safe, Secure and
                  Interoperable Smart Devices: Proceedings of the
                  International Workshop CASSIS~2004},
  PAGES = {1--26},
  YEAR = 2005,
  SERIES = {LNCS~3362},
  PUBLISHER = {Springer},
  URL = {http://www.inf.ed.ac.uk/~stark/mrg-smart-devices.html},
  PDF = {http://www.inf.ed.ac.uk/~stark/mrg-smart-devices.pdf}
}

@INPROCEEDINGS{ghani-icfp05,
  THEME = {B},
  AUTHOR = {Neil Ghani and
               Patricia Johann and
               Tarmo Uustalu and
               Varmo Vene},
  TITLE = {Monadic augment and generalised short cut fusion.},
  BOOKTITLE = {International Conference on Functional Programming (ICFP05)},
  ADDRESS = {Tallinn, Estonia},
  MONTH = SEP,
  YEAR = {2005},
  PAGES = {294--305},
  URL = {http://www.cs.ioc.ee/~tarmo/papers/icfp05.pdf}
}

@INPROCEEDINGS{sannella+:mrg-evaluation,
  AUTHOR = {Donald Sannella and Martin Hofmann and David Aspinall and
                  Stephen Gilmore and Ian Stark and Lennart Beringer and
                  Hans-Wolfgang Loidl and Kenneth MacKenzie and Alberto
                  Momigliano and Olha Shkaravska},
  TITLE = {Mobile Resource Guarantees (evaluation paper) },
  BOOKTITLE = {TFP~2005: Proceedings of the 6th Symposium on Trends in
                  Functional Programming},
  PAGES = {7--16},
  YEAR = 2005,
  OPTPDF = {http://www.cs.ioc.ee/tfp-icfp-gpce05/tfp-proc/01num.pdf},
  OPTURL = {http://www.cs.ioc.ee/tfp-icfp-gpce05/tfp-proc/},
  URL = {http://groups.inf.ed.ac.uk/mrg/publications/mrg/mrg-sum.pdf}
}

@INPROCEEDINGS{DBLP:conf/fsttcs/LagoH05,
  AUTHOR = {Ugo Dal Lago and
               Martin Hofmann},
  TITLE = {{Quantitative Models and Implicit Complexity}},
  BOOKTITLE = {Foundations of Software Technology and Theoretical Computer Science (FSTTCS05)},
  YEAR = {2005},
  SERIES = {LNCS~3821},
  PUBLISHER = {Springer},
  PAGES = {189-200},
  EDITORS = {R. Ramanujam and Sandeep Sen},
  ADDRESS = {Hyderabad, India},
  MONTH = DEC,
  URL = {http://www.appsem.org/papers/Dal_Lago_Hofmann_FSTTCS.pdf}
}

@INPROCEEDINGS{ReusStreicher:ICALP,
  AUTHOR = {B. Reus and Th. Streicher},
  TITLE = {About Hoare Logics for Higher-order Store},
  BOOKTITLE = {Proceedings of the 32th Intern.\ Conference on Automata, Languages, and Programming Languages (ICALP05)},
  YEAR = {2005},
  SERIES = {LNCS~3580},
  EDITOR = {Lu\'is Caires and Giuseppe F. Italiano and Lu\'is Monteiro  and Catuscia Palamidessi and Moti Yung},
  OPTVOLUME = {3580},
  PAGES = {1337--1348},
  URL = {http://www.cogs.susx.ac.uk/users/bernhard/PapersFolder/ICALP05.pdf}
}

@INPROCEEDINGS{Reus:Schwinghammer:05,
  AUTHOR = {B. Reus and J. Schwinghammer},
  TITLE = {Denotational Semantics for {Abadi} and {Leino}'s Logic of Objects},
  BOOKTITLE = {European Symposium on Programming (ESOP05)},
  YEAR = {2005},
  EDITOR = {Mooly Sagiv},
  PAGES = {263--278},
  SERIES = {LNCS~3444},
  OPTSERIES = {Lecture Notes in Computer Science},
  PUBLISHER = {Springer Verlag},
  URL = {http://www.cogs.susx.ac.uk/users/bernhard/PapersFolder/etaps05.pdf}
}

@INPROCEEDINGS{PattinsonReus:2005,
  AUTHOR = {Dirk Pattinson and Bernhard Reus},
  TITLE = {{A Complete Temporal and Spatial Logic for Distributed Systems}},
  EDITORS = {Bernhard Gramlich},
  BOOKTITLE = {Frontiers of Combining Systems (FroCoS)},
  SERIES = {Lecture Notes in Artificial Intelligence},
  VOLUME = {3717},
  YEAR = {2005},
  PAGES = {122--137},
  PUBLISHER = {Springer},
  ADDRESS = {Berlin},
  URL = {http://www.cogs.susx.ac.uk/users/bernhard/PapersFolder/FroCos05.pdf}
}

@INPROCEEDINGS{danielssonetal06:fastandloose,
  AUTHOR = {Nils Anders Danielsson and Jeremy Gibbons and John
                  Hughes and Patrik Jansson},
  TITLE = {{Fast and Loose Reasoning is Morally Correct}},
  BOOKTITLE = {{Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium
                  on Principles of Programming Languages (POPL06)}},
  YEAR = {2006},
  MONTH = JAN,
  NOTE = {ACM SIGPLAN Notices, Vol~41(1)},
  PAGES = {206--217},
  SUMMARY = {http://www.cs.chalmers.se/~nad/publications/danielsson-et-al-popl2006.html},
  URL = {http://www.cs.chalmers.se/~nad/publications/danielsson-et-al-popl2006.pdf}
}

@ARTICLE{HylandM:cattfe,
  AUTHOR = {Martin Hyland and Misao Nagayama and John Power and
                  Giuseppe Rosolini},
  TITLE = {A {C}ategory {T}heoretic {F}ormulation for
                  {E}ngeler-style {M}odels of the {U}ntyped
                  {$\lambda$}-{C}alculus},
  VOLUME = {161},
  PAGES = {43--57},
  YEAR = {2006},
  JOURNAL = {Electronic Notes in Theoretical Computer Science},
  NOTE = {Proceedings of MFCSIT},
  URL = {http://www.appsem.org/papers/Hyland.pdf}
}

@INPROCEEDINGS{Mogelberg:LAPLsdt:MFPS,
  AUTHOR = {R. E. M{\o}gelberg and L. Birkedal and G. Rosolini},
  TITLE = {Synthetic domain theory and models of linear {A}badi \& {P}lotkin logic},
  YEAR = 2005,
  BOOKTITLE = {Proceedings of the Twenty-first Conference on the Mathematical Foundations of Programming Semantics},
  PAGES = {219--245},
  VOLUME = 155,
  OPTYEAR = {2005},
  JOURNAL = {Electronic Notes in Theoretical Computer Science},
  URL = {http://www.itu.dk/~birkedal/papers/sdt-lapl-mfps.pdf}
}

@INPROCEEDINGS{abel05:_untyp_algor_equal_martin_logic,
  AUTHOR = {Andreas Abel and Thierry Coquand},
  TITLE = {{Untyped Algorithmic Equality for Martin-L{\"o}f's Logical Framework with Surjective Pairs}},
  BOOKTITLE = {{Typed Lambda Calculi and Applications (TLCA'05)}},
  PAGES = {23--38},
  YEAR = 2005,
  SERIES = {LNCS~3461},
  ADDRESS = {Nara, Japan},
  URL = {http://www.tcs.informatik.uni-muenchen.de/~abel/lfsigma.pdf}
}

@INPROCEEDINGS{abel05:_verif_haskel_progr_using_const_type_theor,
  AUTHOR = {Andreas Abel and  Marcin Benke and Ana Bove and John Hughes and Ulf Norell},
  TITLE = {{Verifying Haskell Programs Using Constructive Type Theory}},
  BOOKTITLE = {{Haskell Workshop (Haskell'05)}},
  YEAR = 2005,
  ADDRESS = {Tallinn, Estonia},
  MONTH = SEP,
  URL = {http://www.tcs.informatik.uni-muenchen.de/~abel/haskell05.ps.gz}
}

@INPROCEEDINGS{abel05:_connec_logic_framew_first_order_prover,
  AUTHOR = {Andreas Abel and Thierry Coquand and Ulf Norell},
  TITLE = {{Connecting a Logical Framework to a First-Order Prover}},
  BOOKTITLE = {{5th International Workshop on Frontiers of Combining Systems (FroCoS'05)}},
  YEAR = 2005,
  ADDRESS = {Vienna, Austria},
  MONTH = SEP,
  URL = {http://www.tcs.informatik.uni-muenchen.de/~abel/haskell05.ps.gz}
}

@ARTICLE{PittsAM:monsf,
  AUTHOR = {M. R. Shinwell and A. M. Pitts},
  TITLE = {On a Monadic Semantics for Freshness},
  JOURNAL = {Theoretical Computer Science},
  YEAR = {2005},
  VOLUME = 342,
  PAGES = {28--55},
  URL = {http://www.cl.cam.ac.uk/~amp12/papers/monsf/monsf-jv.pdf}
}

@INPROCEEDINGS{laud05:_type,
  AUTHOR = {P. Laud and T. Uustalu and V. Vene},
  TITLE = {Type systems equivalent to dataflow analyses for imperative languages},
  BOOKTITLE = {{3rd APPSEM II Workshop (APPSEM '05)}},
  YEAR = 2005,
  ADDRESS = {Frauenchiemsee, Germany},
  MONTH = SEP,
  NOTE = {To appear in TCS},
  URL = {http://www.cs.ioc.ee/~tarmo/papers/appsem05-tcs.pdf}
}

@ARTICLE{DybjerSetzer,
  AUTHOR = {Peter Dybjer and Anton Setzer},
  TITLE = {{Indexed induction-recursion}},
  JOURNAL = {Journal of Logic and Algebraic Programming},
  YEAR = 2006,
  VOLUME = 66,
  NUMBER = 1,
  PAGES = {1--49},
  MONTH = {January},
  URL = {http://www.cs.chalmers.se/~peterd/papers/Indexed\_IR.ps.gz}
}

@INPROCEEDINGS{GhaniTFP06,
  AUTHOR = {N.~Ghani and M.~Hamana and T.~Uustalu and V.~Vene},
  TITLE = {{Representing cyclic structures as nested datatypes}},
  BOOKTITLE = {{Proc. of 7th Symp. on Trends in Functional Programming (TFP 2006)}},
  PAGES = {173--188},
  YEAR = 2006,
  ADDRESS = {Nottingham, U.K.},
  MONTH = APR,
  URL = {http://www.cs.ioc.ee/~tarmo/papers/tfp06.pdf}
}

@ARTICLE{GUH2006,
  AUTHOR = {Neil Ghani and Tarmo Uustalu and Makoto Hamana},
  TITLE = {{Explicit substitutions and higher-order syntax}},
  JOURNAL = {{Higher-order and Symbolic Computation}},
  YEAR = 2006,
  VOLUME = 19,
  NUMBER = {2--3},
  PAGES = {263--282},
  URL = {http://www.cs.ioc.ee/~tarmo/papers/merlin03-hosc.pdf}
}


This file has been generated by bibtex2html 1.82.