BRICS Research Series, 1996

April 29, 2003

This document is also available as PostScript and DVI.

References

[RS-96-62] Abstract, PostScript, PDF, DVI.

P. S. Thiagarajan and Igor Walukiewicz. An Expressively Complete Linear Time Temporal Logic for Mazurkiewicz Traces. December 1996. 19 pp. Appears in Twelfth Annual IEEE Symposium on Logic in Computer Science, LICS ’97 Proceedings, 1997, pages 183–194.

[RS-96-61] Abstract, PostScript, PDF, DVI.

Sergei Soloviev. Proof of a Conjecture of S. Mac Lane. December 1996. 53 pp. Extended abstract appears in Pitt, Rydeheard and Johnstone, editors, Category Theory and Computer Science: 6th International Conference, CTCS ’95 Proceedings, LNCS 953, 1995, pages 59–80 Journal version appears in Annals of Pure and Applied Logic, 90(1–3):101–162, 1997.

[RS-96-60] Abstract, PostScript, PDF.

Johan Bengtsson, Kim G. Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi. Uppaal in 1995. December 1996. 5 pp. Appears in Margaria and Steffen, editors, Tools and Algorithms for The Construction and Analysis of Systems: 2nd International Workshop, TACAS ’96 Proceedings, LNCS 1055, 1996, pages 431–434.

[RS-96-59] Abstract, PostScript, PDF.

Kim G. Larsen, Paul Pettersson, and Wang Yi. Compositional and Symbolic Model-Checking of Real-Time Systems. December 1996. 12 pp. Appears in The 16th IEEE Real-Time Systems Symposium, RTSS ’95 Proceedings, 1995, pages 76–89.

[RS-96-58] Abstract, PostScript, PDF.

Johan Bengtsson, Kim G. Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi. Uppaal — a Tool Suite for Automatic Verification of Real–Time Systems. December 1996. 12 pp. Appears in Alur, Henzinger and Sontag, editors, Hybrid Systems III: Verification and Control, LNCS 1066, 1995, pages 232–243.

[RS-96-57] Abstract, PostScript, PDF.

Kim G. Larsen, Paul Pettersson, and Wang Yi. Diagnostic Model-Checking for Real-Time Systems. December 1996. 12 pp. Appears in Alur, Henzinger and Sontag, editors, Hybrid Systems III: Verification and Control, LNCS 1066, 1995, pages 575–586.

[RS-96-56] Abstract, PostScript, PDF. Zine-El-Abidine Benaissa, Pierre Lescanne, and Kristoffer H. Rose. Modeling Sharing and Recursion for Weak Reduction Strategies using Explicit Substitution. December 1996. 35 pp. Appears in Kuchen and Swierstra, editors, Programming Languages, Implementations, Logics, and Programs: 8th International Symposium, PLILP ’96 Proceedings, LNCS 1140, 1996, pages 393–407.

[RS-96-55] Abstract, PostScript.

Kre J. Kristoffersen, Franois Laroussinie, Kim G. Larsen, Paul Pettersson, and Wang Yi. A Compositional Proof of a Real-Time Mutual Exclusion Protocol. December 1996. 14 pp. Appears with the title A Compositional Proof of a Mutual Exclusion Protocol in Bidoit and Dauchet, editors, Theory and Practice of Software Development: 7th International Joint Conference CAAP/FASE, TAPSOFT ’97 Proceedings, LNCS 1214, 1997, pages 565–579.

[RS-96-54] Abstract, PostScript, DVI. Igor Walukiewicz. Pushdown Processes: Games and Model Checking. December 1996. 31 pp. Appears in Alur and Henzinger, editors, Computer-Aided Verification: 8th International Conference, CAV ’96 Proceedings, LNCS 1102, 1996, pages 62–74. Journal version appears in Information and Computation, 164:234–263, 2001.

[RS-96-53] Abstract, PostScript, DVI. Peter D. Mosses. Theory and Practice of Action Semantics. December 1996. 26 pp. Appears in Penczek and Szalas, editors, Mathematical Foundations of Computer Science: 21st International Symposium, MFCS ’96 Proceedings, LNCS 1113, 1996, pages 37–61.

[RS-96-52] Abstract, PostScript, DVI. Claus Hintermeier, Hlne Kirchner, and Peter D. Mosses. Combining Algebraic and Set-Theoretic Specifications (Extended Version). December 1996. 26 pp. Appears in Haveraaen, Owe and Dahl, editors, Recent Trends in Data Type Specification: 11th Workshop on Specification of Abstract Data Types, RTDTS ’95 Selected Papers, LNCS 1130, 1996, pages 255–274.

[RS-96-51] Abstract, PostScript.

Claus Hintermeier, Hlne Kirchner, and Peter D. Mosses. R^{n}- and G^{n}-Logics. December 1996. 19 pp. Appears in Dowek, Heering, Meinke and Mller, editors, Higher-Order Algebra, Logic, and Term-Rewriting: 2nd International Workshop, HOA ’96 Proceedings, LNCS 1074, 1996, pages 90–108.

[RS-96-50] Abstract, PostScript, DVI. Aleksandar Pekeč. Hypergraph Optimization Problems: Why is the Objective Function Linear? December 1996. 10 pp.

[RS-96-49] Abstract, PostScript, DVI. Dan S. Andersen, Lars H. Pedersen, Hans Httel, and Josva Kleist. Objects, Types and Modal Logics. December 1996. 20 pp. Appears in Pierce, editor, 4th International Workshop on the Foundations of Object-Oriented, FOOL4 Proceedings, 1997.

[RS-96-48] Abstract, PostScript, DVI. Aleksandar Pekeč. Scalings in Linear Programming: Necessary and Sufficient Conditions for Invariance. December 1996. 28 pp.

[RS-96-47] Abstract, PostScript, DVI. Aleksandar Pekeč. Meaningful and Meaningless Solutions for Cooperative N-person Games. December 1996. 28 pp.

[RS-96-46] Abstract, PostScript, DVI. Alexander E. Andreev and Sergei Soloviev. A Decision Algorithm for Linear Isomorphism of Types with Complexity Cn(log^{2}(n)). November 1996. 16 pp.

[RS-96-45] Abstract, PostScript. Ivan B. Damgrd, Torben P. Pedersen, and Birgit Pfitzmann. Statistical Secrecy and Multi-Bit Commitments. November 1996. 30 pp. Appears in IEEE Transactions on Information Theory, 44(3):1143– 1151, (1998).

[RS-96-44] Abstract, PostScript, DVI. Glynn Winskel. A Presheaf Semantics of Value-Passing Processes. November 1996. 23 pp. Extended and revised version of paper appearing in Montanari and Sassone, editors, Concurrency Theory: 7th International Conference, CONCUR ’96 Proceedings, LNCS 1119, 1996, pages 98–114.

[RS-96-43] Abstract, PostScript, DVI. Anna Inglfsdttir. Weak Semantics Based on Lighted Button Pressing Experiments: An Alternative Characterization of the Readiness Semantics. November 1996. 36 pp. Appears in van Dalen and Bezem, editors, European Association for Computer Science Logic: 10th Workshop, CSL ’96 Selected Papers, LNCS 1258, 1997, pages 226–243.

[RS-96-42] Abstract, PostScript, DVI. Gerth Stlting Brodal and Sven Skyum. The Complexity of Computing the k-ary Composition of a Binary Associative Operator. November 1996. 15 pp.

[RS-96-41] Abstract, PostScript, DVI. Stefan Dziembowski. The Fixpoint Bounded-Variable Queries are PSPACE-Complete. November 1996. 16 pp. Appears in van Dalen and Bezem, editors, European Association for Computer Science Logic: 10th Workshop, CSL ’96 Selected Papers, LNCS 1258, 1997, pages 89–105.

[RS-96-40] Abstract, PostScript, DVI. Gerth Stlting Brodal, Shiva Chaudhuri, and Jaikumar Radhakrishnan. The Randomized Complexity of Maintaining the Minimum. November 1996. 20 pp. Appears in Nordic Journal of Computing, 3(4):337–351, 1996 (special issue devoted to Selected Papers of the 5th Scandinavian Workshop on Algorithm Theory (SWAT’96)). Appears in Karlson and Lingas, editors, 5th Scandinavian Workshop on Algorithm Theory, SWAT ’96 Proceedings, LNCS 1097, 1996, pages 4–15.

[RS-96-39] Abstract, PostScript, DVI. Hans Httel and Sandeep Shukla. On the Complexity of Deciding Behavioural Equivalences and Preorders – A Survey. October 1996. 36 pp.

[RS-96-38] Abstract, PostScript, DVI. Hans Httel and Josva Kleist. Objects as Mobile Processes. October 1996. 23 pp. Presented at 12th Annual Conference on the Mathematical Foundations of Programming Semantics, MFPS ’96 Proceedings (Boulder, Colorado, USA, June 3–5, 1996)), TCS, 1996.

[RS-96-37] Abstract, PostScript, DVI. Gerth Stlting Brodal and Chris Okasaki. Optimal Purely Functional Priority Queues. October 1996. 27 pp. Appears in Journal of Functional Programming, 6(6):839–858, November 1996.

[RS-96-36] Abstract, PostScript, DVI. Luca Aceto, Willem Jan Fokkink, and Anna Inglfsdttir. On a Question of A. Salomaa: The Equational Theory of Regular Expressions over a Singleton Alphabet is not Finitely Based. October 1996. 16 pp. Appears in Theoretical Computer Science, 209(1–2):141–162, December 1998.

[RS-96-35] Abstract, PostScript, DVI. Gian Luca Cattani and Glynn Winskel. Presheaf Models for Concurrency. October 1996. 16 pp. Appears in van Dalen and Bezem, editors, European Association for Computer Science Logic: 10th Workshop, CSL ’96 Selected Papers, LNCS 1258, 1997, pages 58–75.

[RS-96-34] Abstract, PostScript, PDF, DVI. John Hatcliff and Olivier Danvy. A Computational Formalization for Partial Evaluation (Extended Version). October 1996. 67 pp. Appears in Mathematical Structures in Computer Science, 7(5):507– 541, October 1997.

[RS-96-33] Abstract, PostScript.

Jonathan F. Buss, Gudmund Skovbjerg Frandsen, and Jeffrey Outlaw Shallit. The Computational Complexity of Some Problems of Linear Algebra. September 1996. 39 pp. Revised version appears in Reischuk and Morvan, editors, 14th Annual Symposium on Theoretical Aspects of Computer Science, STACS ’97: Proceedings, LNCS 1200, 1997, pages 451–462 and later in Journal of Computer and System Sciences, 58(3):572–596, 1998.

[RS-96-32] Abstract, PostScript, DVI. P. S. Thiagarajan. Regular Trace Event Structures. September 1996. 34 pp.

[RS-96-31] Abstract, PostScript, DVI. Ian Stark. Names, Equations, Relations: Practical Ways to Reason about ‘new’. September 1996. ii+22 pp. Please refer to the revised version BRICS-RS-97-39.

[RS-96-30] Abstract, PostScript, DVI. Arne Andersson, Peter Bro Miltersen, and Mikkel Thorup. Fusion Trees can be Implemented with AC^{0} Instructions only. September 1996. 8 pp. Appears in Theoretical Computer Science, 215(1–2):337– 344, 1999.

[RS-96-29] Abstract, PostScript. Lars Arge. The I/O-Complexity of Ordered Binary-Decision Diagram Manipulation. August 1996. 35 pp. An extended abstract version appears in Staples, Eades, Kato and Moffat, editors, 6th International Symposium on Algorithms and Computation, ISAAC ’95 Proceedings, LNCS 1004, 1995, pages 82–91.

[RS-96-28] Abstract, PostScript. Lars Arge. The Buffer Tree: A New Technique for Optimal I/O Algorithms. August 1996. 34 pp. This report is a revised and extended version of the BRICS Report RS-94-16. An extended abstract appears in Akl, Dehne, Sack and Santoro, editors, Algorithms and Data Structures: 4th Workshop, WADS ’95 Proceedings, LNCS 955, 1995, pages 334–345.

[RS-96-27] Abstract, PostScript, DVI. Devdatt P. Dubhashi, Volker Priebe, and Desh Ranjan. Negative Dependence Through the FKG Inequality. July 1996. 15 pp.

[RS-96-26] Abstract, PostScript, DVI. Nils Klarlund and Theis Rauhe. BDD Algorithms and Cache Misses. July 1996. 15 pp.

[RS-96-25] Abstract, PostScript, DVI. Devdatt P. Dubhashi and Desh Ranjan. Balls and Bins: A Study in Negative Dependence. July 1996. 27 pp. Appears in Random Structures and Algorithms 13(2):99–124, 1998.

[RS-96-24] Abstract, PostScript. Henrik Ejersbo Jensen, Kim G. Larsen, and Arne Skou. Modelling and Analysis of a Collision Avoidance Protocol using SPIN and UPPAAL. July 1996. 20 pp. Appears in Grgoire, Holzmann and Peled, editors, The Spin Verification System: 2nd International SPIN Workshop, SPIN ’96 Proceedings, American Mathematical Society Press (AMS) DIMACS Series in Discrete Mathematics and Theoretical Computer Science, 1997, pages 33–47.

[RS-96-23] Abstract, PostScript, DVI. Luca Aceto, Willem Jan Fokkink, and Anna Inglfsdttir. A Menagerie of Non-Finitely Based Process Semantics over BPA^{∗}: From Ready Simulation Semantics to Completed Tracs. July 1996. 38 pp.

[RS-96-22] Abstract, PostScript, DVI. Luca Aceto and Willem Jan Fokkink. An Equational Axiomatization for Multi-Exit Iteration. June 1996. 30 pp. Appears in Information and Computation, 137(2):121–158, 1997.

[RS-96-21] Abstract, PostScript, DVI. Dany Breslauer, Tao Jiang, and Zhigen Jiang. Rotation of Periodic Strings and Short Superstrings. June 1996. 14 pp. Appears in Journal of Algorithms, 24(2):340–353, August 1997.

[RS-96-20] Abstract, PostScript, DVI. Olivier Danvy and Julia L. Lawall. Back to Direct Style II: First-Class Continuations. June 1996. 36 pp. A preliminary version of this paper appeared in the proceedings of the 1992 ACM Conference on Lisp and Functional Programming, William Clinger, editor, LISP Pointers, Vol. V, No. 1, pages 299–310, San Francisco, California, June 1992. ACM Press.

[RS-96-19] Abstract, PostScript, DVI. John Hatcliff and Olivier Danvy. Thunks and the λ-Calculus. June 1996. 22 pp. Appears in Journal of Functional Programming 7(3):303–319 (1997).

[RS-96-18] Abstract, PostScript, DVI. Thomas Troels Hildebrandt and Vladimiro Sassone. Comparing Transition Systems with Independence and Asynchronous Transition Systems. June 1996. 14 pp. Appears in Montanari and Sassone, editors, Concurrency Theory: 7th International Conference, CONCUR ’96 Proceedings, LNCS 1119, 1996, pages 84–97.

[RS-96-17] Abstract, PostScript, DVI. Olivier Danvy, Karoline Malmkjr, and Jens Palsberg. Eta-Expansion Does The Trick (Revised Version). May 1996. 29 pp. Appears in ACM Transactions on Programming Languages and Systems, 8(6):730–751, 1996.

[RS-96-16] Abstract, PostScript, DVI. Lisbeth Fajstrup and Martin Rauen. Detecting Deadlocks in Concurrent Systems. May 1996. 10 pp. Appears in Sangiorgi and de Simone, editors, Concurrency Theory: 9th International Conference, CONCUR ’98 Proceedings, LNCS 1466, 1998, pages 332–347.

[RS-96-15] Abstract, PostScript, DVI. Olivier Danvy. Pragmatic Aspects of Type-Directed Partial Evaluation. May 1996. 27 pp. Appears in Danvy, Glck and Thiemann, editors, Partial Evaluation: International Seminar, PE ’96 Selected Papers, LNCS 1110, 1996, pages 73–94.

[RS-96-14] Olivier Danvy and Karoline Malmkjr. On the Idempotence of the CPS Transformation. May 1996. 17 pp.

[RS-96-13] Abstract, PostScript, DVI.

Olivier Danvy and Ren Vestergaard. Semantics-Based Compiling: A Case Study in Type-Directed Partial Evaluation. May 1996. 28 pp. Appears in Kuchen and Swierstra, editors, Programming Languages, Implementations, Logics, and Programs: 8th International Symposium, PLILP ’96 Proceedings, LNCS 1140, 1996, pages 182–197.

[RS-96-12] Abstract, PostScript.

Lars Arge, Darren Erik Vengroff, and Jeffrey Scott Vitter. External-Memory Algorithms for Processing Line Segments in Geographic Information Systems. May 1996. 34 pp. To appear in Algorithmica. A shorter version of this paper appears in Spirakis, editor, Third Annual European Symposiumon on Algorithms, ESA ’95 Proceedings, LNCS 979, 1995, pages 295–310.

[RS-96-11] Abstract, PostScript, DVI.

Devdatt P. Dubhashi, David A. Grable, and Alessandro Panconesi. Near-Optimal, Distributed Edge Colouring via the Nibble Method. May 1996. 17 pp. Appears in Spirakis, editor, Third Annual European Symposiumon on Algorithms, ESA ’95 Proceedings, LNCS 979, 1995, pages 448–459. Appears in the special issue of Theoretical Computer Science, 203(2):225–251, August 1998, devoted to the proceedings of ESA ’95.

[RS-96-10] Abstract, PostScript, DVI.

Torben Braner and Valeria de Paiva. Cut-Elimination for Full Intuitionistic Linear Logic. April 1996. 27 pp. Also available as Technical Report 395, Computer Laboratory, University of Cambridge.

[RS-96-9] Abstract, PostScript, DVI.

Thore Husfeldt, Theis Rauhe, and Sren Skyum. Lower Bounds for Dynamic Transitive Closure, Planar Point Location, and Parentheses Matching. April 1996. 11 pp. Appears in Nordic Journal of Computing, 3(4):323–336, December 1996. Also in Karlson and Lingas, editors, 5th Scandinavian Workshop on Algorithm Theory, SWAT ’96 Proceedings, LNCS 1097, 1996, pages 198–211.

[RS-96-8] Abstract, PostScript, DVI.

Martin Hansen, Hans Httel, and Josva Kleist. Bisimulations for Asynchronous Mobile Processes. April 1996. 18 pp. Abstract appears in BRICS Notes Series NS-94-6, pages 188–189. Appears in Tbilisi Symposium on Language, Logic, and Computation (Tbilisi, Republic of Georgia, October 19–22, 1995).

[RS-96-7] Abstract, PostScript, DVI.

Ivan B. Damgrd and Ronald Cramer. Linear Zero-Knowledge - A Note on Efficient Zero-Knowledge Proofs and Arguments. April 1996. 17 pp. Appears in The Twenty-ninth Annual ACM Symposium on Theory of Computing, STOC ’97 Proceedings, 1997, pages 436–445.

[RS-96-6] Abstract, PostScript, DVI. Mayer Goldberg. An Adequate Left-Associated Binary Numeral System in the λ-Calculus (Revised Version). March 1996. 19 pp. Appears in Journal of Functional Programming 10(6):607–623, 2000. This report is a revision of the BRICS Report RS-95-42.

[RS-96-5] Abstract, PostScript, DVI. Mayer Goldberg. Gdelisation in the λ-Calculus (Extended Version). March 1996. 10 pp Appears in Information Processing Letters 75(1– 2):13–16, 2000. Earlier version Also available as BRICS Report RS-95-38.

[RS-96-4] Abstract, PostScript, DVI. Jrgen H. Andersen, Ed Harcourt, and K. V. S. Prasad. A Machine Verified Distributed Sorting Algorithm. February 1996. 21 pp. Abstract appeared in Bjerner, Larsson and Nordstrm, editors, 7th Nordic Workshop on Programming Theory, NWPT ’7 Proceedings, Programming Methodology Group’s Report Series Report 86, January 1996, 1995, pages 62–82.

[RS-96-3] Abstract, PostScript, DVI. Jaap van Oosten. The Modified Realizability Topos. February 1996. 17 pp. Appears in Journal of Pure and Applied Algebra, 116:273–289, 1997 (the special Freyd issue).

[RS-96-2] Abstract, PostScript, DVI. Allan Cheng and Mogens Nielsen. Open Maps, Behavioural Equivalences, and Congruences. January 1996. 25 pp. A short version of this paper appeared in Kirchner, editor, Trees in Algebra and Programming: 21st International Colloquium, CAAP ’96 Proceedings, LNCS 1059, 1996, pages 257–272, and a full version appears in Theoretical Computer Science, 190(1):87–112, January 1998.

[RS-96-1] Abstract, PostScript, DVI. Gerth Stlting Brodal and Thore Husfeldt. A Communication Complexity Proof that Symmetric Functions have Logarithmic Depth. January 1996. 3 pp.