[ToC] ==================\=====================/====== AMAST Links 02 08 _____________________ \ / _____________________ Contributions are / \ AMAST Links / \ 9 January 1996 welcome! e-mail to ( / \ ) e-mailed to: amast@cs.utwente.nl \ / Vol. 02 Issue 08 \ / 799 subscribers ^^^^^^^^^^^^^^^^^^^^^ ^^^^^^^^^^^^^^^^^^^^^ ^^^^^^^^^^^^^^^^^^^^^ An index to all issues of the AMAST newsletter is available on the WWW: URL: http://www.cs.utwente.nl/data/amast/links/AL-Index.html A general index to AMAST information on the WWW server in Twente is at: URL: http://www.cs.utwente.nl/data/amast/Index.html The hypertext version of this issue is available at: URL: http://www.cs.utwente.nl/data/amast/links/v02/i08/AL0208-ToC.html _________________ Table of Contents Meetings [M1] 3rd AMAST Workshop on Real-Time Systems, ARTS'96 (upd. [AL0207C1]) [M2] 8th Lipari Int'l School for CS Researchers, _Computer Graphics_ [M3] ERCIM Workshop on Computer-Supported Cooperative Work and the Web [M4] ISSTA'96 and Workshop FMSP'96, Advance Program (upd. [AL0205C5]) CfPs [C1] AMAST'96, Call for Systems Demo's, ext. deadline (upd. [AL0206C1]) [C2] Pract Appl Int Agents & Multi-Agent Tech, PAAM'96 (upd [AL0207CK]) [C3] 9th IFIP Int'l Workshop Testing of Communicating Systems, IWTCS'96 [C4] Annual Conf. of European Assoc. for Computer Science Logic, CSL'96 [C5] IFIP Joint Conf. Formal Techniques & Protocol Spec., FORTE/PSTV'96 [C6] 7th Int'l Conference on Concurrency Theory, CONCUR'96 [C7] Verification of Infinite State Systems (Satellite W. of CONCUR'96) [C8] 11th Symp. on Logic in Computer Science, LICS'96 (upd. [AL0207C3]) [C9] 3rd Int'l Colloquium on Grammatical Inference, ICGI'96 [CA] 8th I. Conf. Computer-Aided Verification, CAV'96 (upd. [AL0207C2]) [CB] 3rd Workshop on Designing Correct Circuits, DCC'96 [CC] 12th W. Mathematical Foundations of Programming Semantics, MFPS'96 [CD] 8th Int'l Conference on Automata and Formal Languages, ICAFL'96 Jobs [J1] Position in Formal Semantics, U. Illinois, Urbana-Champaign, USA [J2] Position available, Math. Dep't, Tulane U., New Orleans, LA, USA [J3] Research Fellow, Math. Dep't, Univ. Twente, Enschede, NL [J4] Chairperson, Dep't of Math. & CS, Kent State Univ., Kent, OH, USA [J5] Faculty Positions, Dep't of Math. Sciences, U. of Memphis, TN, USA [J6] Chair Position, Dep't of Math. Sciences, U. of Memphis, TN, USA [J7] Postdoctoral Fellowship, School of Math. & Stat., U. of Sydney, AU [J8] Postdoctoral Fellowships, MPI, U. des Saarlandes, Saarbr"ucken, D [J9] Postdoctoral Position, Dep't of CS, Duke Univ., Durham, NC, USA [JA] Assistant Researcher Position, U. du Littoral, Dunkerque-Calais, F Literature [L1] Book: Specification and Validation Methods [L2] Book: Reasoning About Knowledge [L3] Paper: On the Equivariant 2-type of a G-space [L4] Paper: Full Abstraction for PCF [L5] Paper: Semantical Investigations of Linear Logic [L6] Paper: A Type-Theoretic Basis for an OO Refinement Calculus [L7] Paper: Typing in OO languages: Achieving Expressibility and Safety Tools [T1] Esterel v4_45 Now Available [T2] The Fc2Tools Verification Toolset Problems [P1] Power of Basic Parallel Processes Services [S1] Algebraic Methods in Language Processing, on WWW (upd. [AL0207M1]) [S2] New WWW Page on Logic-Related Conferences [S3] FLIRTS Workshop and WWW page [S4] WWW page Evolving Algebras Europe [S5] WWW Bibliography on HOL Theorem Proving [S6] Formal Methods Tools database Archive [A1] New items in the AMAST information repository in Twente [A2] This issue [M1] ================================================ AMAST Links 02 08 Third International AMAST Workshop on Real-Time Systems, ARTS'96 Models, Properties and Control Salt-Lake City, Utah, USA, March 6-8, 1996 *Update* of information in [AL0207C1]. The latest announcement is available at URL: http://www.cs.utwente.nl/data/amast/links/v02/i08/full/AC0208M1.txt The latest announcement of the 3rd AMAST Workshop on Real-Time Systems gives new information about the invited speakers and their talks. Potential participants are urged to send a notice of intent for participation as soon as possible; this will help the organizers to make accommodation arrangements accordingly. [M2] ================================================ AMAST Links 02 08 8th Int'l School for Computer Science Researchers - "Computer Graphics" Lipari Island, Italy, June 30 - July 13, 1996 The full version of this announcement is available at URL: http://www.cs.utwente.nl/data/amast/links/v02/i08/full/AC0208M2.txt The Eighth School for Computer Science Researchers addresses PhD students and young researchers who want to get exposed to the forefront of research activity in the field of Computer Graphics. The school will be held in the beautiful surroundings of the Island of Lipari which can be reached by ferry from Naples, Milazzo, Messina, Reggio Calabria and Palermo. The official language is English. Six courses will be offered of which each student must choose four. A proficiency final exam at the end of each chosen course is mandatory. Saturday of the first week will be entirely dedicated to open research problems and discussion. Registration fee is 300 US dollars per person. A limited number of fellowships covering the registration fee will be reserved to partecipants who must afford high travelling expenses. A maximum of thirty students will be allowed. See the full version of this announcement for application details. *Courses:* Procedural Methods in Texturing and Animation, Ken Perlin (N.Y. U.) Dynamic Constraints, Andy Witkin (Carnegie Mellon U.) Augmented Reality for Visualization, Steven K. Feiner (Columbia U.) Splined Curves & Surface Using Polar Forms, L.J. Guibas (Stanford U) Methods in Computer Graphic Modeling, John F. Hughes (Brown U.) Real Time Simulation Systems, Randy Pausch (U. of Virginia) *Directors:* Alfredo Ferro, Dipartimento di Matematica, University of Catania Ken Perlin, Computer Science Department, New York University e-mail: SCHOOL@DIPMAT.UNICT.IT *Sponsors:* Under the auspices of E.A.C.S.L. - European Association for Computer Science Logic A.I.L.A - Associazione Italiana Logica ed Applicazioni [M3] ================================================ AMAST Links 02 08 International Workshop "CSCW and the Web" Sankt Augustin, Germany, February 7-9, 1996 The full version of this _Call for Participation_ is located at URL: http://www.cs.utwente.nl/data/amast/links/v02/i08/full/AC0208M3.txt The ERCIM World-Wide Web Working Group (W4G) and GMD invite you to participate in an open international workshop on support for collaboration on the Web. Computer-Supported Cooperative Work (CSCW) has been an issue of active research for more than a decade. The World-Wide Web offers unique possibilities as an underlying infrastructure to support collaborative work across the internet. On the other hand, the architecture of the Web imposes some barriers to CSCW applications that are hard to overcome. Over the last year, Web-based collaborative applications have started to emerge. The aims of this workshop are to establish contacts between people with an active interest in this field and to learn from each other's experiences about the opportunities and problems involved in the design, construction, and deployment of Web-based systems to support collaboration. Also, the results of the workshop may feed into the work that is carried out by INRIA and ERCIM on behalf of W3C. Persons involved in research on the topic of this workshop (whether from a CSCW or from a WWW background) are particularly encouraged to participate. See the full version of this announcement for more information. *Important dates:* Presentations have to be submitted before January 5. Workshop participants should register before January 25. *Registration:* Persons who want to give a presentation should submit an extended abstract, briefly describing what they want to present. Persons who want to participate and not give a presentation are encouraged to submit a position paper stating their background and interest in the workshop. See the full version for more details. The size of the workhop is limited to 40 participants. The registration fee is DM 100,- (VAT included) If you are interested in participating in this workshop, please mail to David Kerr (kerr@gmd.de). [M4] ================================================ AMAST Links 02 08 ISSTA'96 and FMSP'96, Advance Program Hyatt Islandia, San Diego, California, USA, January 8-11, 1996 *Update* of information in [AL0205C5]. The _ISSTA'96 & FMSP'96 Advance Program_ is available at URL: http://www.cs.utwente.nl/data/amast/links/v02/i08/full/AC0208M4.txt ISSTA'96: Int'l Symp. on Software Testing & Analysis, Jan. 8-10 FMSP'96: Workshop on Formal Methods in Software Practice, Jan. 10-11 Sponsored by ACM SIGSOFT. ISSTA'96 brings together researchers and practitioners to present and discuss research in software testing and analysis. Presentations will cover a wide range of topics, including new theoretical models and techniques, empirical results and experience, and software tools. This year, a special workshop track within the symposium allows timely presentation of work in progress, and of analyses, reviews, and opinions on the state of software testing and analysis. The purpose of FMSP'96 is to bring together experts in formal methods technology and the early innovators in industry who have adopted formal methods. Discussions will focus on the impact of formal methods on software practice, as well as on strategies to further this impact in the future. This workshop is being co-located with ISSTA'96 to encourage the cross-pollination of ideas between the formal methods and the testing communities. Attendance at both meetings is open to all. Up-to-date information will be maintained at the following Web sites: ISSTA'96 : http://www.cs.ucsb.edu/Conferences/ISSTA96 FMSP'96 : http://xenon.stanford.edu/~sankar/FMSP96 [C1] ================================================ AMAST Links 02 08 5th Int'l Conf. Algebraic Methodology and Software Technology, AMAST'96 M"unich, Germany, July 1-5, 1996 *Update* of the information in [AL0206C1] See full version of this _Call for System Demonstrations_ at URL: http://www.cs.utwente.nl/data/amast/links/v02/i08/full/AC0208C1.txt We invite submissions for system demonstrations showing the effectiveness of software developed on a mathematical basis. The topics of interest include, but are not limited to, the following: o Software Development Environments o Support for Correct Software Development o System Support for Reuse o Tools for Prototypiung, Validation and Verification o Theorem Proving Systems We invite prospective authors to submit 6 copies of system demo proposals (4 double spaced pages maximum) in an area relevant to the conference theme. Papers should provide adequate information for the reviewers to assess the significance and anticipated impact of the system on software technology. All submissions must be sent to Martin Wirsing, AMAST'96 Program Chair, Institut f"ur Informatik, Universit"at M"unchen, Leopoldstr. 11B D-80802 M"unchen, Germany. Phone: ++49/89/ 2180-6317, Fax: ++49/89/ 2180-6310 e-mail: amast96-info@informatik.uni-muenchen.de *Important Dates:* Submission of System Demo Proposals: January 15, 1996 Notification of Acceptance/Rejection: February 1, 1996 Camera-ready Version Accepted System Demo Proposals: March 15, 1996 Submission of Student Research Papers: June 1, 1996 Education Day: July 1, 1996 Conference Days: July 2-5, 1996 *Further Information.* See the full version of this announcement at the URL above, or the _Postscript version_ at the URL: http://www.pst.informatik.uni-muenchen.de/amast96/ or the _plain-text version_ at URL: http://www.cs.utwente.nl/data/amast/amast96/CallForDemos.txt [C2] ================================================ AMAST Links 02 08 Practical Appl. of Intelligent Agents & Multi-Agent Technology, PAAM'96 London, UK, Monday 22nd April - Tuesday 23rd April 1996 *Update* of information in [AL0207CK]. The _Final Call for Papers_ is available at the URL: http://www.cs.utwente.nl/data/amast/links/v02/i08/full/AC0208C2.txt The First International Conference and Exhibition on the Practical Application of Intelligent Agents and MultiAgents is a new conference aiming to demonstrate the use of agent technology for solving real-world problems in business, industry, and commerce. This exciting European Union sponsored event will showcase powerful industrial and commercial applications of agent-based software, and include presentations from leading international companies which are successfully introducing this key technology. *Call for Participation.* You are invited to register your interest for this event by completing the reply form given in the full version of this announcement at the URL above. *Call for Papers.* We invite you to submit a paper or industrial report describing fielded applications which exploit agent technology. Papers can be of any length (up to a maximum of 20 pages), and on virtually any agent related topic. Five copies of papers should be submitted by January 26th 1996. A list of suggested topics and detailed submission information is given in the full version of this announcement at the URL above. *Call for Demonstrations, Workshops and Tutorials.* The conference also provides an opportunity for software vendors and developers to demonstrate Agent systems. You are invited to contact the organiser to arrange for your application to be exhibited at the event. If you would like to organise a workshop or tutorial, or wish to see a particular topic covered, please contact us. To register interest, or for further information on this exciting new conference & exhibition contact: Al Roth, PAAM96 Secretariat, Tel: +44 (0) 1253 358081 Fax: +44 (0) 1253 353811, E-mail: agents@pap.com WWW : http://www.demon.co.uk/ar/PAAM96/index.html [C3] ================================================ AMAST Links 02 08 9th IFIP Int'l Workshop on Testing of Communicating Systems, IWTCS'96 Formerly: International Workshop on Protocol Test Systems Darmstadt, Germany, September 9-11, 1996 The full version of this _Call for Papers_ is available at URL: http://www.cs.utwente.nl/data/amast/links/v02/i08/full/AC0208C3.txt A Postscript version of the full Call for Papers is available via WWW page : http://www.darmstadt.gmd.de/~gattung/iwtcs/iwtcs96.html and anonymous ftp : ftp://ftp.darmstadt.gmd.de/pub/iwtcs96/cfp.ps.gz The aim of this workshop is to bring together researchers and practitioners in the field of testing of communicating systems. *Topics of interest:* o Types of testing: Conformance testing - Interoperability testing - Performance testing o Phases of the testing process: Test case generation - Realization of means of testing - Test execution - Analysis of results o Classes of systems to be tested: OSI protocols and services - Internet protocols and services - Telecommunication networks - ATM networks - Narrowband networks - ODP systems - Multimedia systems o Theory and practice of testing: Theoretical framework - Test-related algorithms - Applications of theory - Practical testing methodology - Practical testing experience *Important dates:* o March 11, 1996 Paper submissions o May 10, 1996 Notification of acceptance o June 17, 1996 Camera-ready copies o June 17, 1996 Proposals for tool demonstrations *Submission policy:* Several types of contributions are solicited: o Regular papers (original research or practice results, maximally 16 pages including bibliography), o Short papers (position statements, work in progress, experience reports, not necessarily original, maximally 5 pages), o Tool demonstrations. Submissions should be sent in 5 copies to one of the co-chairs. *Conference co-chairs:* Bernd Baumgarten, Heinz-J"urgen Burkhardt, Alfred Giessler GMD, Rheinstr. 75, 64295 Darmstadt, Germany [C4] ================================================ AMAST Links 02 08 Annual Conf. of European Association for Computer Science Logic, CSL'96 Utrecht, NL, September 21 - 27, 1996 The full version of this Call for Papers is available in two forms: plain-text (?=txt) and LaTeX (?=tex) respectively at URL: http://www.cs.utwente.nl/data/amast/links/v02/i08/full/AC0208C4.? CSL is the annual conference of the European Association for Computer Science Logic (EACSL). The conference is intended for computer scientists whose research activities involve logic, as well as for logicians working in areas related to computer science. *Scientific Program* September 21 - 22, 1996 Tutorial on Applications of Categorical Logic to Computer Science (Concurrency), organized by I. Moerdijk (Utrecht). Speakers: B. Jacobs (Amsterdam), J. van Oosten (Utrecht), G. Winskel (Aarhus). September 23 - 27, 1996 Invited lectures and contributed papers. *Submissions* Authors are invited to submit five copies of a draft of a full paper (5-12 pages) and twelve copies of a two page abstract to the chairman of the program committee. The cover page should include title, authors, and corresponding author: name, address, phone number, e-mail address, and fax number (if available). The _deadline_ is May 1st 1996. The authors will be notified of acceptance for presentation at the conference by July 13, 1996. Detailed submission information is available in the full version of this announcement at the URL above. *Grants* For young scientists living at least one year in EU-countries some grants are available from the HCM Euroconferences program of the EU. For more information please contact the chair. The final application should be sent not later then May 1, 1996. [C5] ================================================ AMAST Links 02 08 IFIP TC6/WG6.1 Joint International Conference FORTE/PSTV'96 Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification Kaiserslautern, Germany, 8-11 October 1996 The full version of this _Call for Papers_ is available at the URL: http://www.cs.utwente.nl/data/amast/links/v02/i08/full/AC0208C5.txt FORTE/PSTV'96 will address Formal Description Techniques (FDTs) applicable to Communication Protocols and Distributed Systems (such as Estelle, Lotos, SDL, ASN.1, TTCN, Z, Automata, Process Algebras, Logics). The conference will be a forum for presentation of the state of the art in theory, application, tools and industrialization of FDTs, and will provide an excellent orientation for newcomers. For the first time, the hitherto separate conferences FORTE and PSTV will be combined into a joint edition. Research papers and industrial usage reports as well as proposals for tutorials (advanced technology seminars), poster displays and tool demonstrations are solicited. *Submissions* Details for submitting original research papers, tools demonstrations and proposals for tutorials are given in the full version of this announcement at the URL above. *Important dates* April 19, 1996: Submission deadline (for more details, see below) June 24, 1996: Notification of acceptance July 19, 1996: Camera-ready copy for final proceedings due *For further information* FORTE/PSTV'96 Organization Committee, University of Kaiserslautern, P.O. Box 3049, D-67653 Kaiserslautern, Germany, Tel: +49 631 205-3426 (Reinhard Gotzhein), -3287 (Jan Bredereke), -2640 (Fax), E-mail: forte.pstv96@informatik.uni-kl.de To obtain additional information (Postscript copy of the Call for Papers, keyword list, etc.), you may browse our _World-Wide Web pages_ at the URL: http://www.informatik.uni-kl.de/aggotz/forte.pstv96 [C6] ================================================ AMAST Links 02 08 Seventh International Conference on Concurrency Theory, CONCUR'96 Pisa, Italy, August 26-29, 1996 The full version of this _Call for Papers_ is available at the URL: http://www.cs.utwente.nl/data/amast/links/v02/i08/full/AC0208C6.tex The purpose of CONCUR conferences is to bring together researchers, developers and students in order to advance the science of concurrency theory and promote its applications. Interest in the conference is continuously growing, as a consequence of the importance and ubiquity of concurrent systems and applications, and of the scientific relevance of their foundations. *Submissions* Authors are invited to send extended abstracts (in English, up to 15 pages, typeset 12 points) to the PC chairman. Simultaneous submissions to other conferences or journals are not allowed. Electronic submissions are encouraged via e-mail, in the form of uuencoded compressed PostScript(tm) files sent to concur'96@di.unipi.it}; however a printed reference copy should be forwarded anyway by express or courier mail. If e-mail is not used, then _five_ (5) copies of the paper should be sent by express or courier mail. In both cases, a separate text-only message should be directed to concur'96@di.unipi.it, with a single postal and e-mail address for communication, complete title, author(s), affiliation(s) and 200 word abstract. *Program Chair* Ugo Montanari, CONCUR'96, Dipartimento di Informatica, University of Pisa, Corso Italia, 40, I-56100 Pisa, Italy. *Important Dates* Deadline for submissions: March 4, 1996 Notification of acceptance: May 6, 1996 Camera-ready version due: June 10, 1996 For further information on topics of interest and submission details please see the full version of this announcement at the URL above. [C7] ================================================ AMAST Links 02 08 Verification of Infinite State Systems, Infinity'96 A Satellite Workshop of CONCUR'96, Pisa, Italy, August 30, 1996 The full version of this _Call for Papers_ is available at URL: http://www.cs.utwente.nl/data/amast/links/v02/i08/full/AC0208C7.txt The aim of this workshop, which will take place immediately following CONCUR'96, is to provide a forum for researchers interested in the development of mathematical techniques for the analysis of infinite state systems, a topic which has received a concerted effort within the Concurrency Theory community over the past few years. The basis of this effort has been the realization that an understanding of infinite state systems is necessary in order to have a complete picture of general process algebras, Petri nets, or other formalisms incorporating value-passing, real-time, hybrid, and/or probabilistic aspects. Its importance has grown however by the further realization that techniques which are developed for infinite state systems -- particularly structural techniques -- can potentially provide elegant solutions to the state-space explosion problem in the analysis of finite state systems, as well as to classical problems in language theory. Possible topics for inclusion are: decidablility issues for equivalence and model checking over various classes of infinite state systems; complexity results for decidability results; connections and applications to questions in classical automata and formal language theory; and tools and case studies involving nontrivial applications of methods for the analysis of infinite state systems. *Submissions.* Send an extended abstract (not to exceed five pages) outlining ongoing work, *before 30 April, 1996.* See the full version of this announcement for submission details. The committee will select the most appropriate abstracts for presentation during the workshop and make their decisions known by 1 June. For technical questions please contact Bernhard Steffen, Universit"at Passau, 94030 Passau. *Proceedings.* The selected abstracts will be compiled in an informal proceedings in the form of a Passau University research report for distribution at the workshop and as electronic notes in TCS. *More information.* See the WWW page at URL: http://www.uni-passau.de/fmi/lehrstuehle/steffen/cfp/infinity.html [C8] ================================================ AMAST Links 02 08 Eleventh Annual IEEE Symposium on Logic In Computer Science, LICS'96 New Brunswick, New Jersey, USA, July 27-30, 1996 *Update* of the information in [AL0206C1] The final call for papers is available at: WWW : http://www.research.att.com/lics/ FTP : ftp://research.att.com/dist/lics/ The *Submission Deadline* is expired. *Correction* The postal code of the Program Chair in the original call for papers is incorrect. The correct address is Edmund M. Clarke Department of Computer Science Carnegie Mellon University Pittsburgh, PA 15213, USA [C9] ================================================ AMAST Links 02 08 Third International Colloquium on Grammatical Inference, ICGI'96 Montpellier, France, September 25-27, 1996 The full version of this announcement is available at URL: http://www.cs.utwente.nl/data/amast/links/v02/i08/full/AC0208C9.txt Grammatical Inference (GI) is broadly understood as Machine Learning of Grammars and Languages from data. Traditionally, GI has been studied within several contexts: Information Theory, Formal Languages Theory, Computational Linguistics, Machine Learning, Pattern Recognition, Computational Learning Neural Networks, etc. This multidisciplinary perspective has lead to a lack of a focused research community. ICGI 96 keeps aiming to provide a forum for discussion of principles, theory and applications of all those aspects of Machine Learning that explicitly focus on Grammars and Languages. A list of example topics is given in the full version of this announcement at the URL above. *Important Dates* April 1, 1996: Deadline for submitted papers. June 15, 1996: Notification of acceptance and referees' comments. July 15, 1996: Camera ready copy. *Submissions* Please submit (not via electronic mail) three copies of your full length article (maximum 12 pages, 12 pt. font, including figures, tables, references, etc.) to: L. Miclet, IRISA-ENSSAT BP 447 - 6, Rue de Krampont 22305 LANNION Cedex, France *Further Information* Information on ICGI'96 is available on the WWW at the URL: http://itkwww.kub.nl:2080/itk/Docs/Projects/Walter/icgi.html [CA] ================================================ AMAST Links 02 08 Conference on Computer-Aided Verification, CAV'96 *Update* of information in [AL0207C2]. The full version of this _Call for Papers_ is available at URL: http://www.cs.utwente.nl/data/amast/links/v02/i08/full/AC0208CA.txt This conference is dedicated to the advancement of the theory and practice of computer-assisted formal analysis methods for software and hardware systems. The conference covers the spectrum from theoretical results to concrete applications, with an emphasis on verification tools and the algorithms and techniques that are needed for their implementation. The proceedings of the conference will be published in the Springer-Verlag Lecture Notes in Computer Science series. A list of suggested topics is given in the full version of this announcement at the URL above. The conference is part of the Federated Logic Conference (FLoC), July 27 - August 3, 1996, being hosted by the Center for Discrete Mathematics and Computer Science (DIMACS), Rutgers University, as part of its Special Year on Logic and Algorithms. *Submission Information* The conference will include contributed papers, project and tool presentations, and invited lectures. Submissions may be either _Regular Papers_ or _Project and Tool Presentations_. Detailed submission information and addresses are given in the full version of this announcement at the URL above. *Important dates* Submission deadline (firm): January 4, 1996 Notification of acceptance: March 11, 1996 Proceedings version of accepted papers due: April 17, 1996 *Further Information* Plain text and Postscript(tm) versions of this Call for Papers are available: WWW : http://www.cs.cornell.edu/Info/People/tah/cav96.html FTP : ftp://ftp.cs.cornell.edu/pub/tah/Cav96/ [CB] ================================================ AMAST Links 02 08 3rd Workshop on Designing Correct Circuits, DCC'96 Baastad, Sweden, September 2nd - 4th, 1996 The full version of this _Call for Papers_ is available at URL: http://www.cs.utwente.nl/data/amast/links/v02/i08/full/AC0208CB.txt The third workshop on Designing Correct Circuits will be held on 2nd September to 4th September 1996 at Baastad in Southern Sweden. This workshop is being organised by Satnam Singh (Glasgow), Mary Sheeran (Chalmers) and Geraint Jones (Oxford). Relevant topics include but are not limited to: formal hardware design languages, hardware design by transformation, computer-aided design and verification of hardware, high level synthesis and silicon compilation, techniques for the design of FPGA circuits, methods for designing testable circuits, analysis of circuit descriptions, novel VLSI algorithms and architectures, asynchronous circuit design. *Submissions* You are invited to submit four copies of a draft full paper on a relevant subject by Wednesday 31 January 1996. Notification of acceptance will be posted by mid April, and revised papers will be due about six weeks later. The email address for submissions and more information is: dcc-workshop@comlab.ox.ac.uk The most up-to-date information about this workshop can be found on the WWW at the URL: http://www.dcs.gla.ac.uk/~satnam/dcc.html Papers can be sent by post to: DCC'96 Workshop, Satnam Singh, Dept. Computing Science, University of Glasgow, Scotland, G12 8QQ United Kingdom Tel: +44 141 330 4454, Email: satnam@dcs.gla.ac.uk [CC] ================================================ AMAST Links 02 08 Mathematical Foundations of Programming Semantics, MFPS'96 Boulder, Colorado, USA, June 3-5, 1996 The Twelfth Workshop on the Mathematical Foundations of Programming Semantics will take place on the campus of the University of Colorado in Boulder from June 3 to June 5, 1996. This series of meetings has the goal of bringing together mathematicians and theoretical computer scientists to discuss problems of common interest and to explore common areas of research. MFPS has focused particularly on programming semantics and related issues. The invited speakers for MFPS 12 are: Peter Freyd (Penn), Mel Fitting (CUNY), Matthew Hennessy (Sussex), Gerard Huet (Inria), Andre Scedrov (Penn) and Jeannette Wing (CMU). In addition, there will be one special session during the meeting. This is a workshop year for MFPS, which means that the remainder of the program will be made up of talks by participants. The slots for these will be allotted on a first-come, first-served basis. As with past MFPS Workshops, the Proceedings of the meeting will consist of journal-length papers submitted by participants after the meeting. These papers will be published as a special issue of Theoretical Computer Science; as such the papers will be refereed to the usual high standards of TCS. Also, we anticipate funding from the Office of Naval Research. While the funding will be limited, we especially encourage women and minorities, as well as graduate students, to inquire about possible support to attend the meeting. *Further Information* More detailed information is available on the WWW at the URL: http://www.math.tulane.edu/MFPS.html See also the home page for _announcements about MFPS 12_ at the URL: http://www.math.tulane.edu/mfps12.html Those who do not have access to the World Wide Web can obtain information by sending email to mfps@math.tulane.edu. If you are interested in attending the meeting and giving a talk, send email to mfps@math.tulane.edu including your name, the title of your talk and a short abstract. Detailed information about registration, lodging, etc. will be sent to those who indicate their interest as soon as available. [CD] ================================================ AMAST Links 02 08 8th International Conference on Automata and Formal Languages, ICAFL'96 Salg'otarj'an, Hungary, July 29 (Mon) - August 2 (Fri), 1996 The full version of this _Call for Papers_ is available at URL: http://www.cs.utwente.nl/data/amast/links/v02/i08/full/AC0208CD.tex The Conference is the continuation of the series of the former "Salgotarjan Conferences", held between 1980 and 1993, in the beautiful montains around Salg\'otarj\'an (in Northern Hungary, about 120 km NE of Budapest, near the Slovakian border), initiated and organized by the late Professor Istv'an Pe'ak (1936-1989). *Submissions.* Those participants who wish to give a talk (20-25 min) are requested to submit o an extended abstract (prefer. max. 2 pages), before March 15, 1996; o the complete paper, based on the talk, before August 2, 1996. Simultaneous submission of a paper to any other conference with published proceedings is not allowed. Authors will be notified of acceptance/rejection by November 30, 1996. See the full version of this announcement for submission details. (Please use electronic mail whenever appropriate, including submission of source files.) The *conference proceedings*, containing the extended abstract, will be distributed to the participants at the beginning of the conference. The *accepted complete papers* will be forwarded to the journal _Publicationes Mathematicae_ (Debrecen) by the Advisory Board of the Conference. The Conference Volume, containing the accepted papers, will be sent to the participants when it is printed. *Costs* Estimates are given in the full version of this announcement. The deadline for early registration (at reduced fee) is May 31, 1996. *Invited Speakers.* R.G. Buharajeev ("), P. Erdos, P. Halmos, D. Perrin, G. Pirillo, J.L. Rhodes, H.J. Shyr, I. Simon ("). (where (") means not yet confirmed). *More Information.* A second announcement is due to appear before the middle of March 1996, and will contain more detailed information about the scientific program, accomodation, and a list of participants. *Pre-registration.* Prospective participants should complete the Form as given in the full version of this announcement and send it as soon as possible but not later than February 15, 1996. [J1] ================================================ AMAST Links 02 08 Assistant Professor Position in Formal Semantics University of Illinois at Urbana-Champaign Department of Linguistics The Department of Linguistics at the University of Illinois at Urbana-Champaign is seeking a specialist in formal semantics for a position to begin August 21, 1996. This is a full-time, tenure-track position at the assistant professor or junior associate professor level, salary competitive. The position is part of an interdisciplinary cognitive science program at the University of Illinois. Strong research and teaching interest in formal semantics of natural language is required and concomitant interest in related ares of cognitive science is desirable including an interest in relevant computational research and applications. It is expected that candidates will have completed the Ph.D. by 21 August 1996. Vita, description of research interests, reprints, and at least three letters of recommendations should be sent to: Professor Elmer Antonsen Head, Department of Linguistics University of Illinois 4088 Foreign Languages Building 707 S. Mathews Urbana, IL 61801 phone: (217) 244-3065, fax: (217) 333-3466 e-mail: deptling@uiuc.edu Although interviews may begin at any time, applications received by January 31 will be given full consideration, and no offer of appointment will be made before that date. A representative of the department will be at the LSA Meeting in San Diego to collect resumes. The University of Illinois is an Affirmative Action/Equal Opportunity Employer. [J2] ================================================ AMAST Links 02 08 Assistant Professor Mathematics Department Tulane University, New Orleans, USA The full version of this announcement is available at URL: http://www.cs.utwente.nl/data/amast/links/v02/i08/full/AC0208J2.txt Applications are invited for a tenure track position at the Assistant Professor level, beginning in the fall semester of 1996, subject to final budgetary approval. Applications from exceptional candidates for appointment at a higher rank will be considered, particularly from women and minority candidates, but current authorization is only at the Assistant Professor level. Applications will be accepted until a suitable candidate is found. Applicants should have completed the Ph.D. by commencement of employment and provide evidence of excellence in both research and teaching. Applications in all areas of pure and applied mathematics and statistics are welcome. Preference will be given to candidates who show promise of strengthening existing research groups within the department. We are especially interested in applications in the areas of statistics and applied probability. Candidates are expected to be competitive for national grant support. We encourage applications from candidates with postdoctoral experience who have started successful funded research programs. Tulane University is an Affirmative Action/Equal Opportunity Employer which is committed to increasing the diversity of its faculty. Applications should be sent c/o Search Committee, Mathematics Department, Tulane University, New Orleans, LA 70118. E-mail applications are preferred at math@math.tulane.edu, and use of the AMS cover sheet is encouraged. The complete application should include a vitae, statements on research and teaching plans, and three letters of recommendation commenting on both research and teaching. For more information see the full version of this announcement. We offer highly competitive salaries. Further information about the department can be obtained from the Math Department home page at URL: http://www.math.tulane.edu [J3] ================================================ AMAST Links 02 08 Research Fellow Position Department of Applied Mathematics University of Twente Enschede, The Netherlands Applications are invited for a research fellow position at the Department of Applied Mathematics of the University of Twente in Enschede, the Netherlands. The applicant should do research in the area of mathematical programming (e..g., discrete optimization, randomized algorithms, large scale programming with applications in OR and logistics etc. ). The appointment is for a period of 6-12 months. Financial support will be granted in form of a stipend: travel costs from the home place to Twente, housing costs (plus health insurance) in Twente, travel grant for participation at conferences plus a (tax-free) monthly allowance of 900 Dutch guilders. For more information contact: Prof.dr. U. Faigle Department of Applied Mathematics University of Twente P.O.Box 217 7500 AE Enschede The Netherlands e-mail: faigle@math.utwente.nl [J4] ================================================ AMAST Links 02 08 Chair Department of Mathematics and Computer Science Kent State University, Kent, Ohio, USA The full version of this announcement is available at URL: http://www.cs.utwente.nl/data/amast/links/v02/i08/full/AC0208J4.txt Kent State University invites applications and nominations for the position of Chairperson of the Department of Mathematics and Computer Science. The Department houses programs through doctoral level in Applied Mathematics, Computer Science, Pure Mathematics, Statistics. Applicants for the position must have an earned doctorate, an international research reputation as evidenced by publications, a successful history of grant activity, and other academic and scholarly achievements. In view of the composition of the department, applicants should have a strong research reputation among both computer scientists and mathematical scientists. They must have the ability and vision to guide the department by developing and maintaining in both disciplines a strong program of scholarship, publications and grantsmanship, an effective advising system, and a strong teaching program. In addition, applicants should have the ability to work well within the university community and to foster interdisciplinary research and cooperation with industry. The successful applicant will be encouraged and supported in maintaining an active research program. Screening of applicants will begin February 1, 1996, for a start date of July 1, 1996, and will continue until the position is filled. Please submit a full resume, including a list of publications, a statement of interest regarding the post, and the names, addresses, telephone numbers and e-mail addresses of at least five references, or a letter of nomination to Chairperson Search Committee, Department of Mathematics and Computer Science, Kent State University, Kent, Ohio 44242, USA, or fax (216)-672-7824. Further information about the Department is available on the World Wide Web at URL: http://www.mcs.kent.edu/ Questions and enquiries can be sent by e-mail to: chair-search@mcs.kent.edu . Kent State University is an Affirmative Action/Equal Opportunity Employer. [J5] ================================================ AMAST Links 02 08 Faculty Positions Department of Mathematical Sciences, The University of Memphis The full version of this announcement is available at URL: http://www.cs.utwente.nl/data/amast/links/v02/i08/full/AC0208J5.txt The Department of Mathematical Sciences invites applications for two tenure-track faculty positions in Computer Science at the assistant and associate professor ranks. Applicants for the junior position are expected to demonstrate exceptional promise in research and teaching; applicants at the senior level are expected to have a strong and ongoing record of research and to be committed to excellence in teaching at all levels. Successful candidates will be expected to provide instruction in a number of broad areas in computer science. Candidates should have a Ph.D. in computer science or in a closely related field. While applicants are welcome from any area in computer science, those active in computer networks and performance analysis, databases, parallel and distributed computing, object-oriented languages and systems, computer graphics, software engineering, scientific computing are particularly sought. Current active areas of research in the department include: Algorithms and complexity, autonomous agents, distributed processing, neural networks, and random number generators. The Department currently has some 35 permanent faculty members in pure and applied mathematics, computer science, and statistics, of which eight are in computer science. The research faculty includes a world-class research group in graph theory, an endowed chair in combinatorics, an active research group in dynamical systems, and an applied statistics research group, which has received large grants from NIH and other agencies. For more details see the full version of this announcement. The selection process for this position will begin February 1, 1996, and continue until these positions are filled. For more information see our web pages at URL: http://www.msci.memphis.edu or write or fax to Ms. Lisa Eldin, Department of Mathematical Sciences, The University of Memphis, Memphis, TN 38152; fax: (901) 678-2480. Successful candidates must meet guidelines of the Immigration and Reform Control Act of 1986. [J6] ================================================ AMAST Links 02 08 Chair The University of Memphis Department of Mathematical Sciences The Department of Mathematical Sciences invites applications for the position of chair. The Department includes pure and applied mathematics, computer science, and statistics. It offers degrees at all levels including the Ph.D. and provides a very favorable research environment in terms of library and computing facilities, teaching load, travel opportunities, etc. Applicants may be from any area of the mathematical sciences, and should have a strong and ongoing research record qualifying for appointment as full professor with tenure. We seek applicants who can creatively lead a multidisciplinary group, with evidence of strong administrative skills and a demonstrated commitment to excellence in teaching, research, and other scholarly activities. The University of Memphis (formerly Memphis State University) is the largest of 46 institutions in the Tennessee Board of Regents system, the seventh largest system of higher education in the nation. It is an Equal Opportunity/Affirmative Action University committed to education of a non-racially identifiable student body. Women and minorities are strongly urged to apply. The selection process will begin December 15, 1995 and may continue until the position is filled. The term as chair will begin in Fall 1996. The successful candidate must meet Immigration Reform Act criteria. Applicants should submit a curriculum vitae and names of references to: Chair-Search Committee Department of Mathematical Sciences The University of Memphis Memphis, TN 38152 Jamisonj@hermes.msci.memst.edu For further information about the department you may also consult our web site at URL: http://www.msci.memphis.edu [J7] ================================================ AMAST Links 02 08 Postdoctoral Fellowship University of Sydney, Australia The full version of this announcement is available at URL: http://www.cs.utwente.nl/data/amast/links/v02/i08/full/AC0208J7.txt As a result of a three-year Australian Research Grant awarded to Max Kelly for research into "two-dimensional universal algebra" - by which is meant the study of structures borne, not just by sets, but by categories and the like - there are funds available to support a position of Postdoctoral Fellow at the University of Sydney for three years from the beginning of 1996. Among the good recent sources for getting some flavour of the subject as practised at Sydney are: o R.Blackwell, G.M.Kelly, and A.J.Power, Two-dimensional monad theory, _J. Pure Appl. Algebra_ 59 (1989), 1-41. o G.M.Kelly, S.Lack, and R.F.C.Walters, Coinverters and categories of fractions for categories with structure, _Applied Categorical_ _Structures_ 1 (1993), 95-102. o G.M.Kelly and A.J.Power, Adjunctions whose counits are coequalizers and presentations of finitary enriched monads, _J. Pure Appl. Algebra_ 89 (1993), 163-179. A Ph.D. in mathematics, either awarded or shortly to be awarded, is an essential qualification - as are a general familiarity with modern category theory, including 2-categories and other enriched categories, together with some research experience into categories with structure or higher-dimensional categories, and evidence of an outstanding capacity for the understanding of mathematics at the highest level. Any familiarity with higher-dimensional categories would be an advantage. Further information from Prof. G.M. Kelly, Tel. +61-2-351-3796, email: kelly_m@maths.su.oz.au or from Assoc. Prof. C. Durrant, Tel. +61-2-351-3373, email: durrant_c@maths.su.oz.au Please forward one copy of the application, quoting reference number A48/xx (value of xx not yet known) and including CV, publications list, and the names, addresses and fax numbers of 3 to 5 referees, to: The Personnel Officer (Sciences Group), Carslaw Building FO7, University of Sydney, NSW 2006, Australia or by fax to +61-2-351-5467. Salary: Aus.Dollars 37345-40087. Closing date: 25 January 1996. [J8] ================================================ AMAST Links 02 08 Postdoctoral Fellowship Max-Planck-Institute for Computer Science, Germany The Max-Planck-Institute for Computer Science is located on the campus of the Universit"at des Saarlandes in Saarbr"ucken, Germany. The institute was founded in 1990 and consists, at present, of two research units: Algorithms and Complexity, and Logic of Programming. Research groups for Distributed Systems and Computer Architecture will be added in 1996/97. The research group *Algorithms and Complexity* offers postdoctoral fellowships. A fellowship is awarded for a one or a two year period and amounts to DM 3,200 per month, taxfree. Further information can be obtained from Shiva Chaudhuri (shiva@mpi-sb.mpg.de) or Michiel Smid (michiel@mpi-sb.mpg.de). The main focus of the research group is data structures, graph and network algorithms, computational geometry, parallel algorithms, combinatorial optimization, randomized algorithms, and implementation of algorithms and program libraries. More information is available on WWW at URL: http://www.mpi-sb.mpg.de Applications (including curriculum vitae, list of publications, research plan, names of references with their e-mail addresses, and intended period of stay) should be sent by the *end of February 1996* to Kurt Mehlhorn or Shiva Chaudhuri. Max-Planck-Institut f"ur Informatik Im Stadtwald D-66123 Saarbr"ucken Germany [J9] ================================================ AMAST Links 02 08 Assistant Research Professor Department of Computer Science, Duke University A postdoctoral position at the level of Assistant Research Professor is available starting in 1996 in the Department of Computer Science at Duke University, under the supervision of Profs. Pankaj Agarwal and Jeff Vitter. Duke is an equal opportunity employer. The position, which is contingent upon grant funding, is for one year and can be extended for one or more additional years. Applicants must have clearly demonstrated experience and skills in the design, analysis, and implementation of combinatorial algorithms, especially in the area of geometric algorithms. Teaching responsibilities include one research course per year on a related topic. The position will include membership in the Center for Geometric Computing, a collaborative effort funded by the Army Research Office with participation from researchers at Brown, Duke, and Johns Hopkins Universities. The problems of interest center around large-scale geometric computations. They include development of efficient methods for the design of geometric data structures, for constructing geometric configurations, and for geometric visualization. Apart from pursuing his or her own research interests in geometric computing, the candidate is expected to play a vital role in the development of the software library for geometric computing, in which the amount of data is very large and I/O communication costs dominate. Issues involving memory hierarchies & parallel models of communication will also be considered. Further responsibilities will be to interact with agency scientists and to help prepare contract, technical, and other reports. The candidate will interact with geometric computing groups at Brown, Johns Hopkins, and the Army Research Laboratories. Please send a letter of interest and your CV, and ask three evaluators to send letters of reference, by US Mail or email to Ms. Cathie Caimano Department of Computer Science Duke University, Box 90129, Durham, NC 27708-0129 Email: cac@cs.duke.edu. Tel: (919) 660-6548 To be assured of full consideration, all material including reference letters must arrive by January 31, 1996. [JA] ================================================ AMAST Links 02 08 The Universite du Littoral, Dunkerque-Calais, France Assistant-researcher Position A position of Maitre de Conferences (assistant-researcher) will be available at the Universite du Littoral, Dunkerque-Calais, France, starting from the next academic year. We are particularly interested in applications of people working in category theory and related areas. A basic knowledge of French language and a Ph.D. degree are requested. People interested in such a position should contact us as soon as possible. For more information: Enrico Vitale Laboratoire LANGAL - Faculte de Sciences Universite du Littoral 1 quai Freycinet - B.P. 5526 59379 Dunkerque - FRANCE tel. 0033 - 28237161 fax: 0033 - 28237039 e-mail: vitale@lma.univ-littoral.fr [L1] ================================================ AMAST Links 02 08 Specification and Validation Methods This book, edited by Egon Boerger, Professor of Computer Science, Dipartimento di Informatica, University of Pisa, Italy, is a survey of the state of the art in specification and validation methods, and applies these methods to real-life computing systems. It combines a high-level introduction to the state of the art with the development of new methods for specification and validation of computing systems. The methods are elaborated for challenging and characteristic applications, spanning from semantics of programming languages and their implementation (PROLOG,CLPC(R) and CLAM,C++) to architecture design (VHDL), including also parallel and distributed programs as well as protocols (Kermit for example). The eleven chapters are written in a self-contained way, each by a leading expert. The book is unique for two reasons: it combines a state-of-the-art survey with a systematic presentation of recent advances, based on new ideas and approaches; its themes range from software to hardware design and the proposed methods are applied to specification and validation of complex real-life computing systems. Contents: Introduction; Evolving algebras 1993. Lipari guide; Annotated bibliography on evolving algebras; Program verification and Prolog; CLAM-specifications for provably correct compilation of CLP(R) program; The semantics of the C++ programming language; Verification of parameterized programs VHDL-based system-level hardware design; The Bakery Algorithm: yet another specification and verification; Kermit: specification and verification; Group membership protocol: specification and verification; Specification and verification of VHDL-based system-level hardware design; Specification and verification of Gate-level VHDL models of synchronous and asynchronous circuits. ISBN 0-19-853854-5, 480 pages, Clarendon Press, April 1995. Hardback L65.00 [L2] ================================================ AMAST Links 02 08 Reasoning About Knowledge by Ronald Fagin, Joseph Y. Halpern, Yoram Moses, and Moshe Y. Vardi Reasoning About Knowledge is the first book to provide a general discussion of approaches to reasoning about knowledge and its applications to distributed systems, artificial intelligence, and game theory. It brings ten years of work by the authors into a cohesive framework for understanding and analyzing reasoning about knowledge that is intuitive, mathematically well founded, useful in practice, and widely applicable. The book is almost completely self-contained and should be accessible to readers in a variety of disciplines, including computer science, artificial intelligence, linguistics, philosophy, cognitive science, and game theory. Each chapter includes excercises and bibliographic notes. **Advance praise for Reasoning About Knowledge** "The result of the authors' research bears the twin hallmarks of good science: beauty and utility." -- Vassos Hadzilacos, Computer Science Department, University of Toronto "[Reasoning About Knowledge] is an impressive systematic technical effort, which will no doubt become a standard reference." -- Johan van Benthem, Institute for Logic, Language, and Computation, University of Amsterdam, and Philosophy Department, Stanford University "It is a must for any student or scholar who really wants to understand the logic of knowledge and interactive knowledge, and an ideal text for an advanced course." -- Ariel Rubinstein, Department of Economics, Tel Aviv University and Princeton University "This is without a doubt the definitive book on the topic ... [It] is also a joy to read ... Anyone conducting formal work in multi-agent systems without access to this book will do so at their peril." -- Yoav Shoham, Computer Science Department, Stanford University For more information on this title, and other MIT Press books, please consult our _WWW site_ at URL: http://www-mitpress.mit.edu/ [L3] ================================================ AMAST Links 02 08 On the equivariant 2-type of a $G$-space Manuel Bullejos A classical theorem of Mac Lane and Whitehead states that the homotopy type of a topological space with trivial homotopy at dimensions 3 and greater can be reconstructed from its $\pi_1$ and $\pi_2$, and a cohomology class $k_3\in H^3(\pi_1,\pi_2)$. More recently, Moerdijk and Svensson suggested the possibility of using Bredon cohomology to extend this result to the equivariant case, that is, for spaces $X$ equipped with an action by a fixed group $G$. In this paper we carry out this suggestion and prove an analogue of the classical result in the equivariant case. _This paper is available_ from URL: http://www.ugr.es/~bullejos [L4] ================================================ AMAST Links 02 08 Full Abstraction for PCF by S. Abramsky, R. Jagadeesan and P. Malacaria A complete version of this paper is _now available_ from URL: http://theory.doc.ic.ac.uk/people/Malacaria An intensional model for the programming language PCF is described, in which the types of PCF are interpreted by games, and the terms by certain ``history-free'' strategies. This model is shown to capture definability in PCF. More precisely, every compact strategy in the model is definable in a certain simple extension of PCF. We then introduce an intrinsic preorder on strategies, and show that it satisfies some remarkable properties, such that the intrinsic preorder on function types coincides with the pointwise preorder. We then obtain an order-extensional fully abstract model of PCF by quotienting the intensional model by the intrinsic preorder. This is the first syntax-independent description of the fully abstract model for PCF. (Hyland and Ong have obtained very similar results by a somewhat different route, independently and at the same time.) We then consider the effective version of our model, and prove a Universality Theorem: every element of the effective extensional model is definable in PCF. Equivalently, every recursive strategy is definable up to observational equivalence. [L5] ================================================ AMAST Links 02 08 Semantical investigations of linear logic by A. Ursini This paper is available in hard copy from the author or via _WWW_ at URL: http://www.csl.sri.com/linear/ursini-paper.dvi.gz (the paper may be difficult to print, but previews fine with xdvi). It deals with the phase-like, Kripke and algebraic semantics of commutative, cyclic, non-commutative, classical or intuitionistic linear logics. Author's address: Aldo Ursini, Universita' di Siena Dipartimento di Matematica Via del Capitano 15 53100 Siena - Italy ph: operator: 577-263111 ; direct: 577-263754 fax: 577-263730 email: ursini@unisi.it [L6] ================================================ AMAST Links 02 08 A Type-Theoretic Basis for an Object-Oriented Refinement Calculus Emil Sekerinski The full version of this information is available at URL: http://www.cs.utwente.nl/data/amast/links/v02/i08/full/AC0208L6.txt This paper is available via _ftp_ at URL: ftp://ftp.abo.fi/pub/cs/papers/emil/oorefcalc.ps.gz or via _WWW_ at URL: http://www.abo.fi/~esekerin This paper addresses the issue of giving a formal semantics to an object-oriented programming and specification language. Object-oriented constructs considered are objects with attributes and methods, encapsulation of attributes, subtyping, bounded type parameters, classes, and inheritance. Classes are distinguished from object types. Besides usual imperative statements, specification statements are included. Specification statements allow changes of variables to be described by a predicate. They are abstract in the sense that they are non-executable. Specification statements may appear in method bodies of classes, leading to abstract classes. The motivation for this approach is that abstract classes can be used for problem-oriented specification in early stages and later refined to efficient implementations. Various refinement calculi provide laws for procedural and data refinement, which can be used here for class refinement. This paper, however, focuses on the semantics of object-oriented programs and specifications and gives some examples of abstract and concrete classes. The semantics is given by a translation of the constructs into the type system Fsub, an extension of the simple typed lambda-calculus by subtyping and parametric polymorphism: The state of a program is represented by a record. A state predicate is a Boolean valued function from states. Statements, both abstract and concrete, are represented by predicate transformers. Objects are represented by records of statements (the methods) operating on a record of attributes. Classes are understood as templates for the creation of objects. Classes are represented by records. Inheritance amounts to record overwriting. Subtyping and parametric polymorphism are already provided by Fsub. [L7] ================================================ AMAST Links 02 08 Typing in object-oriented languages: Achieving expressibility and safety Kim B. Bruce Williams College While simple static-typing disciplines exist for object-oriented languages like C++, Object Pascal, and Modula-3, they are often so restrictive that programmers are forced to by-pass the type system with type casts. Other languages allow more freedom, but require run-time checking to pick up the type errors that their more permissive systems missed. This paper consists of a survey of problems (illustrated by a series of sample programs) with existing type systems, and suggests ways of improving the expressibility of these systems while retaining static type safety. In particular we will discuss the motivations behind introducing "MyType", "matching", and "bounded matching" into these type systems. We also suggest a way of simplifying the resulting type system by replacing subtyping by a type system with a new type construct based on matching. Both systems provide support for binary methods, which are often difficult to support in statically-typed languages. The intent is to avoid pages of type-checking rules and formal proofs, but instead explain why the problems are interesting via the series of sample programs. The technical details (including proofs of subject reduction and type safety) are available elsewhere. The paper is available by following links from my _home page_ URL: http://www.cs.williams.edu/~kim/ or by anonymous ftp from URL: ftp://cs.williams.edu/pub/kim/ as file Static.{dvi,ps}. Comments are welcomed. (An earlier draft version of this paper available on the net was entitled: "Problems with static typing in object-oriented languages". Please discard any copies of the earlier version.) [T1] ================================================ AMAST Links 02 08 The Esterel V4_45 System Available The full version of this announcement is available at URL: http://www.cs.utwente.nl/data/amast/links/v02/i08/full/AC0208T1.txt Esterel v4_45 differs in the following ways from its predecessor Esterelv4_41: o A new causal interpretation scheme has been added (option -I). This interpretation option produces object C code that is much simpler and much faster than the one produced by option -I of esterelv4_41, which uses the Esterel v3 technology. The interpreter is based on a new semantics called the constructive semantics. o The Motif-based graphical simulator xsimul is replaced by a new Tcl/Tk based simulator called xes (X Esterel Simulator). Xes is directly included in the esterelv4_45 distribution tape, unlike xsimul that was distributed separately. o Generation of hardware circuits from Pure Esterel programs is possible by using the -Lblif option (esterel -Lblif foo.strl). The circuits are generated in Berkeley Logic Interchange format (blif). o The wristwatch example is included in the distribution tape. Use it to try xes! Esterel v4_45 is in fact an intermediate version that will later be replaced by Esterel v5 described below. Even if it is yet incomplete, we make it available to let users experiment with the new interpreter and with the xes simulator. If you already ftp'ed an Esterel v4_4x compiler, you will find v4_45 _at the same place_ on URL: ftp://cma.cma.fr with xes included. Just ftp it; you won't need another licence. Otherwise, please write to esterel-request@cma.cma.fr. Gerard Berry, Xavier Fornari, Jean-Paul Marmorat [T2] ================================================ AMAST Links 02 08 Fc2Tools Verification Toolset Available Fc2Tools is a major rewriting of previous (and still existing) Auto/Graph, a popular verification software for concurrent systems based on process algebra results and finite model properties. The most striking features of Fc2Tools are: o A modular toolsuite design, based on common file representation format (Fc2) for description of communicating automata and networks of such; o Simple graphical edition, and process-algebra style interpretation (with Autograph); o Combined or redundant implementations using both implicit and explicit representation methods for finite state models, whatever fits best a given case; o verification by compositional reductions and abstraction of models, avoiding state explosion as much as possible. Current distribution is available for Sun4OS4, and soon on DEC-Alpha architecture. All information can be obtained from URL: http://cma.cma.fr:80/Verification/verif-eng.html or by emailing to: fc2team@cma.cma.fr Enjoy, Amar Bouali, Annie Ressouche, Valerie Roy, Robert de Simone. [P1] ================================================ AMAST Links 02 08 Power of Basic Parallel Processes Philippe Schnoebelen Basic parallel processes (BPP) form a restricted class of processes (here transition systems) which strictly enlarge regular (or finite state) processes but still retain good decidability properties. For example it is decidable whether two BPPs are bisimilar (Christensen, Hirshfeld and Moller). I am interested in what can and what cannot be described with BPPs. Today, all I am aware of is that they are more powerful than finite-state systems and less powerful than labeled P/T petri nets. (Here "powerful" is in the bisimilarity sense, but other criteria may be interesting too.) Where can I find more ? [S1] ================================================ AMAST Links 02 08 AMAST WWW-page on Algebraic Methods in Language Processing, AMiLP *Update* of information in [AL0207M1]. On December 6th until December 8th, the tenth international Twente Workshop on Language Technology (TWLT-10) took place at the University of Twente, Enschede, Netherlands. This workshop was organized by the Computer Science Department in the framework provided by the AMAST movement. The First AMAST Workshop on Language Processing was organized in Enschede, jointly with TWLT-10, and focused on algebraic methods in formal languages, programming languages and natural languages. The aim of this workshop was to bring together researchers on formal language theory, programming language theory and natural language description theory, who have a common interest in the use of algebraic methods to describe syntactic, semantic and pragmatic properties of language. The workshop did not concentrate on natural language only. There is interesting use of algebraic methods in programming language processing (compiler construction and development of programming language environments) and (obviously) in formal language theory. Moreover, it is becoming clear that some of the methods developed in these fields can play a role in natural language description and processing. As a byproduct of the workshop, and to foster further cooperation on the investigation of algebraic methods in language processing (AMiLP), a WWW page on AMiLP will be set-up and maintained at the University of Twente, as a part of the AMAST repository. The starting point for the AMiLP project consists of the current information out of the AMiLP'95 workshop, that is available through the _AMiLP'95 WWW page_ at URL: http://www.cs.utwente.nl/data/amast/workshops/AMiLP95.html That information consists of the following items: 1. The TWLT Proceedings series 2. The AMiLP'95 organization 3. The AMiLP'95 program/time schedule 4. The abstracts of the invited talks A participants' proceedings volume was available at the workshop, and can be ordered from the SETI secretariat (see item 1 at the URL above). [S2] ================================================ AMAST Links 02 08 Logic-Related Conferences There is a new WWW page for logic-related conferences at URL: http://www.research.att.com/lics/logic-confs.html Over the last few years there has been a proliferation of conferences that overlap in their technical scope with the Symposium on Logic in Computer Science (LICS). These conferences are scheduled with no prior coordination among them, which results quite often in conflicts. For example, in 1995 LICS and FPCA were at exactly the same time and the same place with no prior coordination. In an attempt to address this situation, the LICS organization will maintain a WWW page of conferences (including workshops) that have an overlap with logic in computer science. The first half of the page is a list of conferences and associated contacts. The second half is an incomplete list of dates, some tentative and some fixed, for upcoming meetings of these conferences. If you are an organizer of one of these conferences and have some information you would like included in the page, please send mail to lics-request@research.att.com. [S3] ================================================ AMAST Links 02 08 FLIRTS: Formalism Logic Institution Relating, Translating & Structuring DISI, University of Genoa, I, 26-28 October 1995 A *really* informal workshop to discuss together what's going on in the field of logical frameworks (institutions and similar formalisms), focusing on the use of the different kinds of arrows to relate, translate and combine logical components, has been held at DISI (University of Genova) last October. The original "call for participation" has been sent (hopefully) to all people involved in research in the area of institutions and analogous metatheories, with encouragements to forward the message to other interested scientists. A second meeting on FLIRTS is planned for next year, although the organizative details have still to be fixed. If you are interested in receiving information about next FLIRTS (and were not contacted for the first) please send an email to cerioli@disi.unige.it. The meeting has been organized in loose sessions focusing on a subject, during which talks, discussions and brain-storming took place without tight schedule. The sessions included: o Maps between logical frameworks. Speakers: Andrzej Tarlecki on Moving between logical systems, and Maura Cerioli on Mapping logical systems. o Alternative formalisms. Speakers: Cristina Sernadas on Signature morphisms considered harmful: adjunctions between logics, and Uwe Wolter on Are there reasons for a concept like Institutional Frame? o Which new FLIES are needed to FLIRTS? - Syntax-driven methods. Speakers: Till Mossakowsky on Is there a common notion of FLIRTS?, and Jose' Luiz Fiadeiro on Mapping between categories of theories in different institutions. o Constructions of logical frameworks (part I). Speakers: Elena Zucca on Building institutions of dynamic data-types, and Gianna Reggio on Operations for Modularly Defining Institutions. o Constructions of logical frameworks (part II). Speaker: Wieslaw Pawlowski on Institutions with Contexts. More information about FLIRTS is available at URL: http://www.disi.unige.it/staff/cerioli/www/flirtshome.html [S4] ================================================ AMAST Links 02 08 WWW Page on Evolving Algebras I have the pleasure to announce a new WWW page on evolving algebras, _Evolving Algebras Europe_, which is now available at URL: http://www.uni-paderborn.de/cs/eas.html This is in addition to the existing evolving algebra WWW page at the University of Michigan at URL: http://www.eecs.umich.edu/ealgebras/ Both evolving algebra pages offer relevant information on current research and upcoming events. Moreover, they also provide access to written material addressing theoretical foundations, applied systems analysis, and tool support. Evolving algebras have been used with considerable success for the specification and verification of various kinds of discrete dynamic systems including architectures, languages, and protocols of sequential, distributed, and real-time systems. Uwe Glaesser, glaesser@uni-paderborn.de [S5] ================================================ AMAST Links 02 08 HOL Bibliography Available I have recently put together a fairly large bibliography of papers on the theory and applications of Higher Order Logic theorem proving using the HOL system. You can access the bibliography on the World Wide Web, and it includes many hyperlinks to abstracts or actual papers. There is also a separate list of dissertations based around HOL. My intention in compiling this bibliography was to provide a useful resource for people doing theorem-prover research and applications based on HOL or other similar systems. For example, the list should provide beginning researchers (e.g. Ph.d. or M.Sc. students) with a summary of useful starting points for HOL-based research. To gain access to the _bibliography_, point your Web browser at URL: http://www.dcs.gla.ac.uk/~tfm/hol-bib.html And, for _dissertations_, only at URL: http://www.dcs.gla.ac.uk/~tfm/hol-theses.html You can also gain access through my little _HOL page_ at URL: http://www.dcs.gla.ac.uk/~tfm/fmt/hol.html Please feel free to send additions or corrections by email. If there is enough demand, I'll investigate the options for making the bibliography searchable. Tom Melham [S6] ================================================ AMAST Links 02 08 Formal Methods Tools database Updated details of the Formal Methods Tools database can be obtained from the following locations: NCL-UK : ftp://chopwell.ncl.ac.uk/pub/fm_tools/fm_tools_db Soton-UK : ftp://ftp.ecs.soton.ac.uk/pub/packages/fmtools/fmtools.txt Waikato-NZ : ftp://ftp.cs.waikato.ac.nz/pub/formal_methods/fm_tools_db Stanford : ftp://www-formal.stanford.edu/pub/clt/FMTDB/fm_tools_db Updated instructions for sending details of FM tools for the database are at the head of the database, but at _Stanford_ at URL: ftp://www-formal.stanford.edu/pub/clt/FMTDB/fm_tools_db-instructions There is now no charge for anyone since we are about to get EC support for maintaining the database for the next 18 months. The database is now much easier to read. It is presented in two formats: the first is human readable and the second is with fields separated by tabs for loading into your favourite database application. Since there are only 31 entries, the former will probably be the most useful for the present. More sites, especially in the European Community, are desired. Anyone who can offer a site, please e-mail me. Updates are planned every three months. Anyone wishing to have details of their tool put into the database, please read the instructions available from one of the above sites or e-mail me. Tim Denvir [A1] ================================================ AMAST Links 02 08 New items in AMAST repository at CS Faculty of University of Twente := http://www.cs.utwente.nl/data/amast/ := ftp://ftp.cs.utwente.nl/pub/doc/amast/ Date: 09/01/1996 Contents: Index.html, README, amast96/, workshops/, info/, links/, sigala/, amast95/, amast93/, amast91/ amast96/ : AMAST'96 Conference: Call for Systems Demonstrations, ... Contents : CallForDemos.txt, ... workshops/ : AMAST Workshops: o 1st AMAST Workshop on Language Processing AMiLP'95 (WWW page) o 3rd AMAST Workshop on Real-Time Systems, ARTS'96 (Final announcement and Call for Papers) Contents : AMiLP95.html, AMAST-RTW96CfP.txt amilp95/ : information on the AMiLP'95 workshop, joint with the 10th Twente Workshop on Language Technology (TWLT), available via the AMiLP'95 WWW page (see above) info/ : records of communication onto the AMAST mailing list Contents : ..., ady02/, ... ady02/ : digests of messages sent onto the AMAST mailing list in 1995; two digests are available: o last digest of messages distributed on the list o cumulative annual digest for the current year Contents : ADY02N13 [26/09/1995--10/11/1995] CAADY02 [01/01/1995--10/11/1995] links/ : AMAST newsletter Contents : AL-Index.html, v02/, v01/, sample/ Note : The file AL-Index.html provides WWW users with links to individual issues of the AMAST newsletter (...) v02/ : second volume of AMAST Links (1995) Contents : i08/, i07/, i06/, i05/, i04/, i03/, i02/, i01/ i08/ : AMAST Links Vol. 02, Issue 08 [09/01/1996] full/ [A2] ================================================ AMAST Links 02 08 This issue was edited by Giuseppe Scollo, Arie van Deursen, Michael Johnson, Edmund Kazmierczak and Elena Trichina, thanks to contributions by: [M1] Dan Ionescu [M2] Alfredo Ferro [M3] Uwe Busbach [M4] Sriram Sankar [C1] Bernhard Reus [C2] Al Roth [C3] Olaf Henniger [C4] Mark van Atten [C5] Jan Bredereke [C6] Ugo Montanari [C7] Tiziana Margaria [C8] Amy Felty [C9] Laurent Miclet [CA] Tom Henzinger [CB] Satnam Singh [CC] Michael W. Mislove [CD] Pal D"om"osi [J1] COLIBRI 47-1995 [J2] Michael W. Mislove (see [CC]) [J3] Ulrich Faigle [J4] Paul A. Farrell [J5] -- [J6] -- (see [J5]) [J7] Max Kelly [J8] Michiel Smid [J9] Jeff Vitter [JA] Enrico Vitale [L1] Egon B"orger [L2] Michael Rutter [L3] Manuel Bullejos [L4] Pasquale Malacaria [L5] Aldo Ursini [L6] Emil Sekerinski [L7] Kim Bruce [T1] Gerard Berry [T2] Robert de Simone [P1] Philippe Schnoebelen [S1] Giuseppe Scollo [S2] Doug Howe [S3] Maura Cerioli [S4] Uwe Gl"asser [S5] Tom Melham [S6] Tim Denvir This issue of AMAST Links is available in four forms: o a collection of hypertext files, available on the WWW at URL: http://www.cs.utwente.nl/data/amast/links/v02/i08/AL0208-ToC.html for the ToC-page, where links give access to individual pages; o a single hypertext file, available on the WWW at URL: http://www.cs.utwente.nl/data/amast/links/v02/i08/AL0208.html o a collection of plain-text files, one per page, each separately available (+) (see below) o a single plain-text file available by e-mail as well as (+) within the AMAST directory of the Twente WWW server, at URL http://www.cs.utwente.nl/data/amast/links/v02/i08/AL0208.txt where `' is either `-ToC' (for the ToC-page),or the 2-character page identifier (for one-page files), or empty (whole-issue file). *Note:* This issue will also be available, in all of its four forms, by anonymous ftp from the AMAST repository at the University of Twente. File names will be the same as above, but under the _ftp directory_ at URL: ftp://ftp.cs.utwente.nl/pub/doc/amast/links/v02/i08/ [end] =============================================== AMAST Links 02 08