@string{brics = "{BRICS}"} @string{daimi = "Department of Computer Science, University of Aarhus"} @string{iesd = "Department of Computer Science, Institute of Electronic Systems, Aalborg University"} @string{rs = "Research Series"} @string{ns = "Notes Series"} @string{ls = "Lecture Series"} @string{ds = "Dissertation Series"} @proceedings{BRICS-NS-94-6, title = "Proceedings of the 6th Nordic Workshop on Programming Theory {\em (Aarhus, Denmark, 17--19 October, 1994)}", year = 1994, editor = "Engberg, Uffe H. and Larsen, Kim G. and Mosses, Peter D.", number = "NS-94-6", series = ns, address = daimi, month = dec, organization = brics, note = "v+483pp", abstract = "The Nordic Workshop on Programming Theory brings together researchers from the Nordic and Baltic countries, in order to improve mutual contacts and collaboration. The invited speakers, however, generally come from non-Nordic/Baltic countries. The 6th Nordic Workshop attracted 63 participants. The workshop had three invited talks and 41 submitted talks. This proceedings contains full papers or extended abstracts of the talks. For completeness we have included short abstracts for the few remaining talks.", linkhtmlabs = "", linkps = "" } @techreport{BRICS-NS-94-5, author = "Pitts, Andrew M.", title = "Some Notes on Inductive and Co-Inductive Techniques in the Semantics of Functional Programs, {\em DRAFT VERSION}", institution = brics, year = 1994, type = ns, number = "NS-94-5", address = daimi, month = dec, note = "vi+135 pp", abstract = "These notes were handed out at a course on {\em Inductive and Co-Inductive Techniques in the Semantics of Functional Programs} given by Andrew Pitts, The Computer Laboratory, Cambridge University, while visiting BRICS 21 November -- 2 December 1994. The course material included these notes, the report {\em Relational Properties of Domains} and slides.\bibpar {\bf Course Description}\\ The aim of the course is to describe recent advances in formal techniques for establishing observational equivalence of functional programs. It considers both operational and denotational methods and the relationship between them. One goal is to give an exposition of Howe's method for characterizing observational equivalence as a co-inductively defined ``applicative bisimulation''. Another goal is to describe Freyd's analysis of recursively defined domains in terms of a property of mixed initiality/finality. Applications of this are given to proving correspondence of operational and denotational semantics and to inductive and co-inductive reasoning about ``user-declared'' datatypes.", linkhtmlabs = "", linkpdf = "" } @proceedings{BRICS-NS-94-4, title = "Abstracts of the 6th Nordic Workshop on PROGRAMMING THEORY {\em (Aarhus, Denmark, 17--19 October, 1994)}", year = 1994, editor = "Mosses, Peter D.", number = "NS-94-4", series = ns, address = daimi, month = oct, organization = brics, note = "v+52 pp", abstract = "The Nordic Workshop on Programming Theory brings together researchers from the Nordic and Baltic countries, in order to improve mutual contacts and collaboration. The invited speakers, however, generally come from non-Nordic/Baltic countries. The 6th Nordic Workshop attracted 63 participants. Abstracts of the three invited talks, the 41 submitted talks, and the four system demonstrations, are collected here. A proceedings volume, with full papers by speakers at the workshop, is to appear by the end of 1994. ", linkhtmlabs = "", linkpdf = "" } @proceedings{BRICS-NS-94-3, title = "Complexity Theory: Present and Future {\em (Aarhus, Denmark, 15--18 August, 1994)}", year = 1994, editor = "Skyum, Sven", number = "NS-94-3", series = ns, address = daimi, month = sep, organization = brics, note = "v+213 pp", abstract = "These ``proceedings'' contain slides, overviews and papers on which the conference talks were based.\bibpar The conference was a byproduct of a longer meeting for a relatively small number of researchers in complexity theory, hosted by BRICS, which took place in Aarhus during the months of August and September, 1994.", linkhtmlabs = "", linkpdf = "" } @techreport{BRICS-NS-94-2, author = "Basin, David A.", title = "Induction Based on Rippling and Proof Planning. {M}ini-Course", institution = brics, year = 1994, type = ns, number = "NS-94-2", address = daimi, month = aug, note = "62~pp", abstract = "Mathematical Induction is a central technique in reasoning about programs and their properties, e.g., loops and recursion, recursively defined data-structures, and program termination. For researchers interested in establishing these properties on a computer, such reasoning must be automated or at least partially supported. In this five hour seminar I will cover some of the central issues in automating proof by mathematical induction. In particular, formalisms for mathematical induction, techniques for selecting induction schemata and well-founded orders, rewriting in inductive theorem proving, and applications. The topics will often be illustrated using ideas and techniques that have been developed at Edinburgh and embodied in the CLAM Inductive Theorem Proving System.", linkhtmlabs = "", linkpdf = "" } @proceedings{BRICS-NS-94-1, title = "Proc.\ 1st International Workshop on Action Semantics {\em (Edinburgh, 14 April, 1994)}", year = 1994, editor = "Mosses, Peter D.", number = "NS-94-1", series = ns, address = daimi, month = may, organization = brics, note = "145 pp", abstract = "Actions speak louder than words: Action Semantics is now being used in practical applications! This workshop surveyed recent achievements, demonstrated tools, and coordinated projects. It was open to all.\bibpar Brief abstracts of the presentations were handed out at the workshop. Extended abstracts/full papers were collected afterwards and are now published here.", linkhtmlabs = "", linkpdf = "" }