BRICS Research Series, 1997

April 29, 2003

This document is also available as PostScript and DVI.

References

[RS-97-53] Abstract, PostScript, PDF, DVI.

Olivier Danvy. Online Type-Directed Partial Evaluation. December 1997. 31 pp. Extended version of an article appearing in Third Fuji International Symposium on Functional and Logic Programming, FLOPS ’98 Proceedings (Kyoto, Japan, April 2–4, 1998), pages 271– 295, World Scientific, 1998.

[RS-97-52] Abstract, PostScript, PDF, DVI.

Paola Quaglia. On the Finitary Characterization of π-Congruences. December 1997. 59 pp.

[RS-97-51] Abstract, PostScript, PDF, DVI.

James McKinna and Robert Pollack. Some Lambda Calculus and Type Theory Formalized. December 1997. 43 pp Appears in Journal of Automated Reasoning 23(3–4):373–409 (1999).

[RS-97-50] Abstract, PostScript, PDF, DVI.

Ivan B. Damgrd and Birgit Pfitzmann. Sequential Iteration of Interactive Arguments and an Efficient Zero-Knowledge Argument for NP. December 1997. 19 pp. Appears in Larsen, Skyum and Winskel, editors, 25th International Colloquium on Automata, Languages, and Programming, ICALP ’98 Proceedings, LNCS 1443, 1998, pages 772–783.

[RS-97-49] Abstract, PostScript, PDF, DVI.

Peter D. Mosses. CASL for ASF+SDF Users. December 1997. 22 pp. Appears in Sellink, Editor, 2nd International Workshop on the Theory and Practice of Algebraic Specifications, Electronic Workshops in Computing, ASF+SDF ’97 Proceedings, Springer-Verlag, 1997.

[RS-97-48] Abstract, PostScript, PDF, DVI.

Peter D. Mosses. CoFI: The Common Framework Initiative for Algebraic Specification and Development. December 1997. 24 pp. Appears in Bidoit and Dauchet, editors, Theory and Practice of Software Development: 7th International Joint Conference CAAP/FASE, TAPSOFT ’97 Proceedings, LNCS 1214, 1997, pages 115–137.

[RS-97-47] Abstract, PostScript, PDF. Anders B. Sandholm and Michael I. Schwartzbach. Distributed Safety Controllers for Web Services. December 1997. 20 pp. Appears in Astesiano, editor, Fundamental Approaches to Software Engineering: First International Conference, FASE ’98 Proceedings, LNCS 1382, 1998, pages 270–284.

[RS-97-46] Abstract, PostScript, PDF, DVI. Olivier Danvy and Kristoffer H. Rose. Higher-Order Rewriting and Partial Evaluation. December 1997. 20 pp. Extended version of paper appearing in Nipkow, editor, Rewriting Techniques and Applications: 9th International Conference, RTA ’98 Proceedings, LNCS 1379, 1998, pages 286–301.

[RS-97-45] Abstract, PostScript, PDF, DVI. Uwe Nestmann. What Is a ‘Good’ Encoding of Guarded Choice? December 1997. 28 pp. Revised and slightly extended version of a paper published in Parrow and Palamidessi, editors, 4th Workshop on Expressiveness in Concurrency, EXPRESS ’97 Proceedings, ENTCS 7, 1997. Revised version appears in Information and Computation 156:287–319 (2000).

[RS-97-44] Abstract, PostScript, PDF, DVI. Gudmund Skovbjerg Frandsen. On the Density of Normal Bases in Finite Fields. December 1997. 14 pp. Appears in Finite Fields and Their Applications, 6(1):23–38, 2000.

[RS-97-43] Abstract, PostScript, PDF, DVI. Vincent Balat and Olivier Danvy. Strong Normalization by Type-Directed Partial Evaluation and Run-Time Code Generation (Preliminary Version). December 1997. 16 pp. Appears in Leroy and Ohori, editors, Types in Compilation, 2nd International Workshop, TIC ’98 Proceedings, LNCS 1473, 1998, pages 240–252.

[RS-97-42] Abstract, PostScript, PDF, DVI. Ulrich Kohlenbach. On the No-Counterexample Interpretation. December 1997. 26 pp. Appears in Journal of Symbolic Logic 64(4):1491–1511, 1999.

[RS-97-41] Abstract, PostScript, PDF, DVI. Jon G. Riecke and Anders B. Sandholm. A Relational Account of Call-by-Value Sequentiality. December 1997. 24 pp. Appears in Twelfth Annual IEEE Symposium on Logic in Computer Science, LICS ’97 Proceedings, 1997, pages 258–267. This report is superseded by the later report BRICS RS-99-10.

[RS-97-40] Abstract, PostScript, PDF, DVI. Harry Buhrman, Richard Cleve, and Wim van Dam. Quantum Entanglement and Communication Complexity. December 1997. 14 pp.

[RS-97-39] Abstract, PostScript, PDF, DVI. Ian Stark. Names, Equations, Relations: Practical Ways to Reason about ‘new’. December 1997. ii+33 pp. Appears in Fundamenta Informaticae 33(4):369–396. This supersedes the earlier BRICS Report RS-96-31, and also expands on the paper presented in Groote and Hindley, editors, Typed Lambda Calculi and Applications: 3rd International Conference, TLCA ’97 Proceedings, LNCS 1210, 1997, pages 336–353.

[RS-97-38] Abstract, PostScript, PDF, DVI. Michał Hańćkowiak, Michał Karoński, and Alessandro Panconesi. On the Distributed Complexity of Computing Maximal Matchings. December 1997. 16 pp. Appears in The Ninth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA ’98 Proceedings, 1998, pages 219–225.

[RS-97-37] Abstract, PostScript, PDF, DVI. David A. Grable and Alessandro Panconesi. Fast Distributed Algorithms for Brooks-Vizing Colourings (Extended Abstract). December 1997. 20 pp. Appears in The Ninth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA ’98 Proceedings, 1998, pages 473– 480. Journal version in Journal of Algorithms, 37(1):85–120, 2000.

[RS-97-36] Abstract, PostScript, PDF, DVI. Thomas Troels Hildebrandt, Prakash Panangaden, and Glynn Winskel. Relational Semantics of Non-Deterministic Dataflow. December 1997. 21 pp.

[RS-97-35] Abstract, PostScript, PDF, DVI. Gian Luca Cattani, Marcelo P. Fiore, and Glynn Winskel. A Theory of Recursive Domains with Applications to Concurrency. December 1997. ii+23 pp. A revised version appears in Thirteenth Annual IEEE Symposium on Logic in Computer Science, LICS ’98 Proceedings, 1998, pages 214–225.

[RS-97-34] Abstract, PostScript, PDF, DVI. Gian Luca Cattani, Ian Stark, and Glynn Winskel. Presheaf Models for the π-Calculus. December 1997. ii+27 pp. Appears in Moggi and Rosolini, editors, Category Theory and Computer Science: 7th International Conference, CTCS ’97 Proceedings, LNCS 1290, 1997, pages 106–126.

[RS-97-33] Abstract, PostScript, PDF, DVI. Anders Kock and Gonzalo E. Reyes. A Note on Frame Distributions. December 1997. 15 pp. Appears in Cahiers de Topologie et Gometrie Diffrentielle Catgoriques, 40(2):127–140, 1999.

[RS-97-32] Abstract, PostScript, PDF, DVI. Thore Husfeldt and Theis Rauhe. Hardness Results for Dynamic Problems by Extensions of Fredman and Saks’ Chronogram Method. November 1997. i+13 pp. Appears in Larsen, Skyum and Winskel, editors, 25th International Colloquium on Automata, Languages, and Programming, ICALP ’98 Proceedings, LNCS 1443, 1998, pages 67–78.

[RS-97-31] Abstract, PostScript, PDF. Klaus Havelund, Arne Skou, Kim G. Larsen, and Kristian Lund. Formal Modeling and Analysis of an Audio/Video Protocol: An Industrial Case Study Using Uppaal. November 1997. 23 pp. Appears in The 18th IEEE Real-Time Systems Symposium, RTSS ’97 Proceedings, 1997, pages 2–13.

[RS-97-30] Abstract, PostScript, PDF, DVI. Ulrich Kohlenbach. Proof Theory and Computational Analysis. November 1997. 38 pp. Slightly revised version appeared in Edalat, Jung, Keimel and Kwiatkowska, editors, Third Workshop on Computation and Approximation, COMPROX III Selected Papers, ENTCS 13, 1998, 34 pp.

[RS-97-29] Abstract, PostScript, PDF. Luca Aceto, Augusto Burgueo, and Kim G. Larsen. Model Checking via Reachability Testing for Timed Automata. November 1997. 29 pp. Appears in Steffen, editor, Tools and Algorithms for the Construction and Analysis of Systems: 4th International Conference, TACAS ’98 Proceedings, LNCS 1384, 1998, pages 263–280.

[RS-97-28] Abstract, PostScript, PDF, DVI. Ronald Cramer, Ivan B. Damgrd, and Ueli Maurer. Span Programs and General Secure Multi-Party Computation. November 1997. 27 pp.

[RS-97-27] Abstract, PostScript, PDF, DVI. Ronald Cramer and Ivan B. Damgrd. Zero-Knowledge Proofs for Finite Field Arithmetic or: Can Zero-Knowledge be for Free? November 1997. 33 pp Appears inKrawczyk, editor, Advances in Cryptology: 18th Annual International Cryptology Conference, CRYPTO ’98 Proceedings, LNCS 1462, 1998pp. 424–441.

[RS-97-26] Abstract, PostScript, PDF, DVI. Luca Aceto and Anna Inglfsdttir. A Characterization of Finitary Bisimulation. October 1997. 9 pp. Appears in Information Processing Letters 64(3):127–134, November 1997.

[RS-97-25] Abstract, PostScript, PDF. David A. Mix Barrington, Chi-Jen Lu, Peter Bro Miltersen, and Sven Skyum. Searching Constant Width Mazes Captures the AC^{0} Hierarchy. September 1997. 20 pp. Appears in Morvan, Meinel and Krob, editors, 15th Annual Symposium on Theoretical Aspects of Computer Science, STACS ’98 Proceedings, LNCS 1373, 1998, pages 73–83.

[RS-97-24] Abstract, PostScript, PDF, DVI. Sren B. Lassen. Relational Reasoning about Contexts. September 1997. 45 pp. Appears as a chapter in the book Higher Order Operational Techniques in Semantics, pages 91–135, Gordon and Pitts, editors, Cambridge University Press, 1998.

[RS-97-23] Abstract, PostScript, PDF, DVI. Ulrich Kohlenbach. On the Arithmetical Content of Restricted Forms of Comprehension, Choice and General Uniform Boundedness. August 1997. 35 pp. Slightly revised version appeared in Annals of Pure and Applied Logic, vol.95, pp. 257-285, 1998.

[RS-97-22] Abstract, PostScript, PDF, DVI. Carsten Butz. Syntax and Semantics of the Logic L_{ωω}^{λ}. July 1997. 14 pp. Appears in Notre Dame of Journal Formal Logic, 38(3):374– 384, 1997.

[RS-97-21] Abstract, PostScript, PDF, DVI. Steve Awodey and Carsten Butz. Topological Completeness for Higher-Order Logic. July 1997. 19 pp. Appears in Journal of Symbolic Logic 65(3):1168–1182 (2000).

[RS-97-20] Abstract, PostScript, PDF, DVI. Carsten Butz and Peter T. Johnstone. Classifying Toposes for First Order Theories. July 1997. 34 pp. Appears in Annals of Pure and Applied Logic, 91(1):33-58, January 1998.

[RS-97-19] Abstract.

Andrew D. Gordon, Paul D. Hankin, and Sren B. Lassen. Compilation and Equivalence of Imperative Objects. July 1997. iv+64 pp. This report is superseded by the later report BRICS RS-98-12. Appears also as Technical Report 429, University of Cambridge Computer Laboratory, June 1997. Appears in Ramesh and Sivakumar, editors, Foundations of Software Technology and Theoretical Computer Science: 17th Conference, FST&TCS ’97 Proceedings, LNCS 1346, 1997, pages 74–87.

[RS-97-18] Abstract, PostScript, PDF, DVI. Robert Pollack. How to Believe a Machine-Checked Proof. July 1997. 18 pp. Appears as a chapter in the book Twenty Five Years of Constructive Type Theory, eds. Smith and Sambin, Oxford University Press, 1998.

[RS-97-17] Abstract, PostScript, PDF, DVI. Peter Bro Miltersen. Error Correcting Codes, Perfect Hashing Circuits, and Deterministic Dynamic Dictionaries. June 1997. 19 pp. Appears in The Ninth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA ’98 Proceedings, 1998, pages 556–563.

[RS-97-16] Abstract, PostScript, PDF, DVI. Noga Alon, Martin Dietzfelbinger, Peter Bro Miltersen, Erez Petrank, and Gbor Tardos. Linear Hashing. June 1997. 22 pp. Appears in The Journal of the Association for Computing Machinery, 46(5):667-683. A preliminary version appeared with the title Is Linear Hashing Good? in The Twenty-ninth Annual ACM Symposium on Theory of Computing, STOC ’97 Proceedings, 1997, pages 465– 474.

[RS-97-15] Abstract, PostScript, PDF, DVI.

Pierre-Louis Curien, Gordon Plotkin, and Glynn Winskel. Bistructures, Bidomains and Linear Logic. June 1997. 41 pp. Appears in Plotkin, Stirling and Tofte, editors, Proof, Language, and Interaction: Essays in Honour of Robin Milner, MIT Press, 2000.

[RS-97-14] Arne Andersson, Peter Bro Miltersen, Sren Riis, and Mikkel Thorup. Dictionaries on AC^{0} RAMs: Query Time Θ(\sqrt{log n/ log log n}) is Necessary and Sufficient. June 1997. 18 pp. Appears in 37th Annual Symposium on Foundations of Computer Science, FOCS ’96 Proceedings, 1996, pages 441–450 with the title Static Dictionaries on AC^{0} RAMs: Query Time Θ(\sqrt{(} log n/ log log n)) is Necessary and Sufficient.

[RS-97-13] Abstract, PostScript, PDF, DVI.

Jrgen H. Andersen and Kim G. Larsen. Compositional Safety Logics. June 1997. 16 pp.

[RS-97-12] Abstract, PostScript, PDF, DVI.

Andrej Brodnik, Peter Bro Miltersen, and J. Ian Munro. Trans-Dichotomous Algorithms without Multiplication — some Upper and Lower Bounds. May 1997. 19 pp. Appears in Dehne, Rau-Chaulin, Sack and Tamassio, editors, Algorithms and Data Structures: 5th International Workshop, WADS ’97 Proceedings, LNCS 1272, 1997, pages 426–439.

[RS-97-11] Abstract, PostScript, PDF, DVI.

Kārlis Čerāns, Jens Chr. Godskesen, and Kim G. Larsen. Timed Modal Specification — Theory and Tools. April 1997. 32 pp.

[RS-97-10] Abstract, PostScript, PDF, DVI.

Thomas Troels Hildebrandt and Vladimiro Sassone. Transition Systems with Independence and Multi-Arcs. April 1997. 20 pp. Appears in Peled, Pratt and Holzmann, editors, DIMACS Workshop on Partial Order Methods in Verification, POMIV ’96 Proceedings, American Mathematical Society Press (AMS) DIMACS Series in Discrete Mathematics and Theoretical Computer Science, 1996, pages 273– 288.

[RS-97-9] Abstract, PostScript, PDF, DVI.

Jesper G. Henriksen and P. S. Thiagarajan. A Product Version of Dynamic Linear Time Temporal Logic. April 1997. 18 pp. Appears in Mazurkiewicz and Winkowski, editors, Concurrency Theory: 8th International Conference, CONCUR ’97 Proceedings, LNCS 1243, 1997, pages 45–58.

[RS-97-8] Abstract, PostScript, PDF, DVI.

Jesper G. Henriksen and P. S. Thiagarajan. Dynamic Linear Time Temporal Logic. April 1997. 33 pp. Full version of paper appearing in Annals of Pure and Applied Logic 96(1-3), pp. 187-207 (1999).

[RS-97-7] Abstract, PostScript, PDF, DVI. John Hatcliff and Olivier Danvy. Thunks and the λ-Calculus (Extended Version). March 1997. 55 pp. Extended version of article appearing in Journal of Functional Programming, 7(3):303–319, May 1997.

[RS-97-6] Abstract, PostScript, PDF, DVI. Olivier Danvy and Ulrik P. Schultz. Lambda-Dropping: Transforming Recursive Equations into Programs with Block Structure. March 1997. 53 pp. Extended version of an article appearing in the 1997 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, PEPM ’97 Proceedings (Amsterdam, The Netherlands, June 12–13, 1997), ACM SIGPLAN Notices, 32(12), pages 90–106. This report is superseded by the later BRICS Report RS-99-27.

[RS-97-5] Abstract, PostScript, PDF, DVI. Kousha Etessami, Moshe Y. Vardi, and Thomas Wilke. First-Order Logic with Two Variables and Unary Temporal Logic. March 1997. 18 pp. Appears in Twelfth Annual IEEE Symposium on Logic in Computer Science, LICS ’97 Proceedings, 1997, pages 228–235.

[RS-97-4] Abstract, PostScript, PDF, DVI. Richard Blute, Jose Desharnais, Abbas Edalat, and Prakash Panangaden. Bisimulation for Labelled Markov Processes. March 1997. 48 pp. Appears in Twelfth Annual IEEE Symposium on Logic in Computer Science, LICS ’97 Proceedings, 1997, pages 149–158.

[RS-97-3] Abstract, PostScript, PDF, DVI. Carsten Butz and Ieke Moerdijk. A Definability Theorem for First Order Logic. March 1997. 10 pp. Appears in Journal of Symbolic Logic, 64(3):1028–1036, 1999.

[RS-97-2] Abstract, PostScript, PDF, DVI. David A. Schmidt. Abstract Interpretation in the Operational Semantics Hierarchy. March 1997. 33 pp.

[RS-97-1] Abstract, PostScript, PDF, DVI. Olivier Danvy and Mayer Goldberg. Partial Evaluation of the Euclidian Algorithm (Extended Version). January 1997. 16 pp. Appears in the journal LISP and Symbolic Computation, 10(2):101–111, July 1997.