APPSEM-II Papers

These papers have been produced jointly by APPSEM-II members from different sites over the lifetime of APPSEM-II. A bibliography of papers produced by APPSEM II members is available as Bibtex file here (659 entries in total).

Selected papers from annual workshops of the APPSEM-II network have been published in Theoretical Computer Science:


[1] Michael Abbott, Thorsten Altenkirch, Neil Ghani, and Conor McBride. Derivatives of containers. In Typed Lambda Calculi and Applications (TLCA03), LNCS 2701, pages 16-30, 2003. [ bib | .pdf ]
[2] Andreas Abel, Marcin Benke, Ana Bove, John Hughes, and Ulf Norell. Verifying Haskell Programs Using Constructive Type Theory. In Haskell Workshop (Haskell'05), Tallinn, Estonia, September 2005. [ bib | .ps.gz ]
[3] Andreas Abel and Thierry Coquand. Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs. In Typed Lambda Calculi and Applications (TLCA'05), LNCS 3461, pages 23-38, Nara, Japan, 2005. [ bib | .pdf ]
[4] Andreas Abel, Thierry Coquand, and Ulf Norell. Connecting a Logical Framework to a First-Order Prover. In 5th International Workshop on Frontiers of Combining Systems (FroCoS'05), Vienna, Austria, September 2005. [ bib | .ps.gz ]
[5] Andreas Abel, Ralph Matthes, and Tarmo Uustalu. Iteration and coiteration schemes for higher-order and nested datatypes. Theoretical Computer Science, 33(1-2):327-341, 2005. FOSSACS special issue. [ bib | .pdf ]
[6] T. Altenkirch, M. Abbot, and N. Ghani. Representing Nested Inductive Types using W-types. In International Colloquium on Automata, Languages and Programming (ICALP 2004), LNCS 3142, pages 59-71, Turku, Finland, July 12-16, 2004. Springer. [ bib | .pdf ]
[7] Thorsten Altenkirch and Tarmo Uustalu. Normalization by Evaluation for λ->2. In Functional and Logic Programming (FLOPS04), LNCS 2998, pages 260-275. Springer, 2004. [ bib | .pdf ]
[8] Mauricio Alvarez-Manilla, Achim Jung, and Klaus Keimel. The probabilistic powerdomain for stably compact spaces. TCS: Theoretical Computer Science, 328(3):221-244, 2004. [ bib | .pdf ]
[9] David Aspinall, Stephen Gilmore, Martin Hofmann, Donald Sannella, and Ian Stark. Mobile resource guarantees for smart devices. In Construction and Analysis of Safe, Secure and Interoperable Smart Devices: Proceedings of the International Workshop CASSIS 2004, LNCS 3362, pages 1-26. Springer, 2005. [ bib | .html | .pdf ]
[10] David Aspinall and Martin Hofmann. Dependent types. In Benjamin Pierce, editor, Advanced Topics in Types and Programming Languages, chapter 2, pages 45-86. MIT press, 2005. [ bib | http ]
[11] G. Barthe, M.J. Frade, E. Gimenez, L. Pinto, and T. Uustalu. Type-based termination of recursive definitions. Mathematical Structures in Computer Science, 14(1):97-141, 2004. [ bib | .ps.gz ]
[12] Nick Benton, Andrew Kennedy, Sam Lindley, and Claudio Russo. Shrinking reductions in SML.NET. In Proceedings of the 16th International Workshop on Implementation and Application of Functional Languages (IFL04), LNCS 3474, pages 142-159. Springer, 2004. [ bib | .pdf ]
[13] L. Birkedal, M. Escardo, A. Jung, and G. Rosolini. Recent Developments in Domain Theory. Theoretical Computer Science, 316(1-3), 2004. [ bib ]
[14] L. Birkedal and G. Rosolini. Categories of reflexive graphs. Technical report, The IT University of Copenhagen, 2004. [ bib ]
[15] Richard Bornat, Cristiano Calcagno, Peter O'Hearn, and Matthew Parkinson. Permission accounting in separation logic. In Proceedings of POPL 2005: The 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 259-270, Long Beach, CA, January 2005. ACM SIGPLAN Notices 40(1). [ bib | .pdf ]
[16] Marco Carbone, Mogens Nielsen, and Vladimiro Sassone. A formal model for trust in dynamic networks. In Intl. Conf. on Software Engineering and Formal Methods (SEFM03), pages 54-61. IEEE Computer Society, 2003. [ bib | .pdf ]
[17] L. Cardelli, P. Gardner, and G. Ghelli. Manipulating Trees with Hidden Labels. In Intl Conf on Foundations of Software Science and Computation Structures (FOSSACS03), LNCS 2620, pages 216-232, Warsaw, Poland, April 2003. [ bib | .pdf ]
[18] L. Cardelli, G. Ghelli, and A. D. Gordon. Secrecy and group creation. Information and Computation, 196(2):127-155, Jan 2005. [ bib | .pdf ]
[19] G. Conforti and G. Ghelli. Decidability of freshness, undecidability of revelation. In Proc. of Foundations of Software Science and Computation Structures (FOSSACS04), LNCS 2987, pages 105-120, Barcelona, Spain, March 2004. Springer. [ bib | .pdf ]
[20] G. Conforti, G. Ghelli, P. Manghi, and C. Sartiani. A self-organizing XML P2P database system. In Proc. of Dodicesimo Convegno su Sistemi Evoluti per Basi di Dati (SEBD), LNCS 3268, pages 394-401, Cagliari, Italy, 2004. Springer. [ bib | .pdf ]
[21] Thierry Coquand, Randy Pollack, and Makoto Takeyama. A Logical Framework with Dependently Typed Records. Fundamenta Informaticae, 65(1-2):112-134, 2005. [ bib | .ps.gz ]
[22] Nils Anders Danielsson, Jeremy Gibbons, John Hughes, and Patrik Jansson. Fast and Loose Reasoning is Morally Correct. In Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL06), pages 206-217, January 2006. ACM SIGPLAN Notices, Vol 41(1). [ bib | .pdf ]
[23] Peter Dybjer and Anton Setzer. Indexed induction-recursion. Journal of Logic and Algebraic Programming, 66(1):1-49, January 2006. [ bib | .ps.gz ]
[24] A. Edalat and D. Pattinson. Initial value problems in domain theory. Technical report, Dept of Computing, Imperial College, London, 2003. [ bib ]
[25] A. Edalat and D. Pattinson. Initial value problems in domain theory. In Proceedings of Computability and Complexity in Analysis (CCA03), 2003. [ bib | .ps ]
[26] Abbas Edalat and Dirk Pattinson. A domain theoretic account of picard's theorem. In International Colloquium on Automata, Languages and Programming (ICALP03), 2003. [ bib | .ps ]
[27] Abbas Edalat and Dirk Pattinson. Initial value problems in domain theory. In Vasco Brattka, Matthias Schröder, Klaus Weihrauch, and Ning Zhong, editors, Computability and Complexity in Analysis (CCA03), volume 302 of Informatik Berichte, pages 211-227. FernUniversität in Hagen, August 2003. International Conference, CCA 2003, Cincinnati, USA, August 28-30, 2003. [ bib ]
[28] M. H. Escardó, M. Hofmann, and Th. Streicher. On the non-sequential nature of the interval-domain model of real-number computation. Mathematical Structures in Computer Science, 14(6):803-814, 2004. [ bib | .ps.gz ]
[29] Andrzej Filinski and Henning Korsholm Rohde. Denotational aspects of untyped normalization by evaluation. Theoretical Informatics and Applications, 39(3):423-453, 2005. [ bib | .pdf ]
[30] N. Ghani, M. Hamana, T. Uustalu, and V. Vene. Representing cyclic structures as nested datatypes. In Proc. of 7th Symp. on Trends in Functional Programming (TFP 2006), pages 173-188, Nottingham, U.K., April 2006. [ bib | .pdf ]
[31] Neil Ghani, Patricia Johann, Tarmo Uustalu, and Varmo Vene. Monadic augment and generalised short cut fusion. In International Conference on Functional Programming (ICFP05), pages 294-305, Tallinn, Estonia, September 2005. [ bib | .pdf ]
[32] Neil Ghani and Tarmo Uustalu. Coproducts of Ideal Monads. Journal of Theoretical Informatics and Applications, 38:321-342, 2004. [ bib | .ps.gz ]
[33] Neil Ghani, Tarmo Uustalu, and Makoto Hamana. Explicit substitutions and higher-order syntax. Higher-order and Symbolic Computation, 19(2-3):263-282, 2006. [ bib | .pdf ]
[34] Neil Ghani, Tarmo Uustalu, and Varmo Vene. Build, Augment, Destroy. Universally. In Proceedings of Programming Languages and Systems: Second Asian Symposium, (APLAS04), LNCS 3302, pages 327-341. Springer, 2004. [ bib | .pdf ]
[35] Neil Ghani, Tarmo Uustalu, and Varmo Vene. Generalizing the augment combinator. In Hans-Wolfgang Loidl, editor, Trends in Functional Programming 5, pages 65-78. Intellect, 2006. [ bib | .pdf ]
[36] Matthew Hennessy, Julian Rathke, and Nobuko Yoshida. safeDpi: A language for controlling mobile code. In FOSSACS: International Conference on Foundations of Software Science and Computation Structures, LNCS 2620. Springer, 2004. [ bib | .pdf ]
[37] J.M.E. Hyland, M. Nagayama, and G. Rosolini. Remarks on the finite-powerset functor on relations. Technical report, Univ of Cambridge, 2004. [ bib ]
[38] Martin Hyland, Misao Nagayama, John Power, and Giuseppe Rosolini. A Category Theoretic Formulation for Engeler-style Models of the Untyped λ-Calculus. Electronic Notes in Theoretical Computer Science, 161:43-57, 2006. Proceedings of MFCSIT. [ bib | .pdf ]
[39] Ugo Dal Lago and Martin Hofmann. Quantitative Models and Implicit Complexity. In Foundations of Software Technology and Theoretical Computer Science (FSTTCS05), LNCS 3821, pages 189-200, Hyderabad, India, December 2005. Springer. [ bib | .pdf ]
[40] P. Laud, T. Uustalu, and V. Vene. Type systems equivalent to dataflow analyses for imperative languages. In 3rd APPSEM II Workshop (APPSEM '05), Frauenchiemsee, Germany, September 2005. To appear in TCS. [ bib | .pdf ]
[41] R. E. Møgelberg, L. Birkedal, and G. Rosolini. Synthetic domain theory and models of linear Abadi & Plotkin logic. In Proceedings of the Twenty-first Conference on the Mathematical Foundations of Programming Semantics, volume 155, pages 219-245, 2005. [ bib | .pdf ]
[42] Matthew Parkinson and Gavin Biermann. Separation logic and abstraction. In Proceedings of POPL 2005: The 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 247-258, Long Beach, CA, January 2005. ACM SIGPLAN Notices 40(1). [ bib | .pdf ]
[43] Dirk Pattinson and Bernhard Reus. A Complete Temporal and Spatial Logic for Distributed Systems. In Frontiers of Combining Systems (FroCoS), volume 3717 of Lecture Notes in Artificial Intelligence, pages 122-137, Berlin, 2005. Springer. [ bib | .pdf ]
[44] B. Reus and J. Schwinghammer. Denotational semantics for Abadi and Leino's logic of objects. In Mooly Sagiv, editor, European Symposium on Programming (ESOP05), LNCS 3444, pages 263-278. Springer Verlag, 2005. [ bib | .pdf ]
[45] B. Reus and Th. Streicher. About hoare logics for higher-order store. In Luís Caires, Giuseppe F. Italiano, Luís Monteiro, Catuscia Palamidessi, and Moti Yung, editors, Proceedings of the 32th Intern. Conference on Automata, Languages, and Programming Languages (ICALP05), LNCS 3580, pages 1337-1348, 2005. [ bib | .pdf ]
[46] G. Rosolini and A. Simpson. Using Synthetic Domain Theory to prove operational properties of a powerful polymorphic language, February 2004. [ bib | .pdf ]
[47] Donald Sannella, Martin Hofmann, David Aspinall, Stephen Gilmore, Ian Stark, Lennart Beringer, Hans-Wolfgang Loidl, Kenneth MacKenzie, Alberto Momigliano, and Olha Shkaravska. Mobile resource guarantees (evaluation paper). In TFP 2005: Proceedings of the 6th Symposium on Trends in Functional Programming, pages 7-16, 2005. [ bib | .pdf ]
[48] M. R. Shinwell and A. M. Pitts. On a monadic semantics for freshness. Theoretical Computer Science, 342:28-55, 2005. [ bib | .pdf ]
[49] Regina Tix, Klaus Keimel, and Gordon D. Plotkin. Semantic domains for combining probability and non-determinism. Electronic Notes in Theoretical Computer Science, 129:1-104, 2005. [ bib | .pdf ]
[50] Christian Urban and James Cheney. Avoiding Equivariance in Alpha-Prolog. In Typed Lambda Calculi and Applications: Proceedings of the Seventh International Conference TLCA 2005, LNCS 3461, pages 401-416. Springer-Verlag, 2005. [ bib | .ps ]
[51] Joost Visser and Joao Saraiva. Tutorial on strategic programming across paradigms. In Proc. 8th Brazilian Symposium on Programming Languages, Niteroi, Brasil, 2004. [ bib ]


This file has been generated by bibtex2html 1.82.