PRELIMINARY PROGRAM and REGISTRATION International Conference on THEORETICAL ASPECTS OF COMPUTER SOFTWARE (TACS'91) September 24-27, 1991 Tohoku University, Sendai, Japan Sponsored by Tohoku University, Sendai, in cooperation with the Information Processing Society of Japan, the Japan Society for Software Science and Technology, the Association for Symbolic Logic, ACM SIGACT and the pending cooperation of the IEEETC on Mathematical Foundations of Computing and ACM SIGPLAN. CONFERENCE CO-CHAIRS Prof. Takayasu Ito Prof. Albert R. Meyer Department of Information Engineering MIT Laboratory for Computer Science Tohoku University 545 Technology Square, NE43-315 Sendai, Japan 980 Cambridge, MA 02139, USA email: tacs91@ito.ecei.tohoku.ac.jp email: tacs-request@theory.lcs.mit.edu FAX: 81 22 267 4404 FAX: (617) 253 3480 PROGRAM COMMITTEE Robert Constable (Cornell U.) Masami Hagiya (Kyoto U.) Susumu Hayashi (Ryukoku U.) Takayasu Ito, Co-Chair (Tohoku U.) J.-L. Lassez (IBM, Yorktown) Albert R. Meyer, Co-Chair (MIT) Gordon D. Plotkin (Edinburgh U.) Amir Pnueli (Weizmann Inst.) Masahiko Sato (Tohoku U.) Dana Scott (Carnegie-Mellon U.) CONFERENCE PROGRAM MONDAY 23 SEPTEMBER Autumnal Equinox Holiday 15:00-20:00 REGISTRATION at Sendai Tokyu Hotel 18:00-19:30 WELCOME RECEPTION at Sendai Tokyu Hotel TUESDAY 24 SEPTEMBER 9:30 OPENING SESSION Takayasu Ito, TACS Co-Chair (Tohoku U.) Albert R. Meyer, TACS Co-Chair (MIT) 10:00 INVITED TALK 1 On the completeness of type-checking Gordon D. Plotkin (Edinburgh U.) 10:50 BREAK 11:20-12:20 SESSION 1 11:20 Type inference in polymorphic type discipline Paola Giannini, Simona Ronchi Della Rocca (U. Torino) 11:50 Monotone recursive definition of predicates and its realizability interpretation Makoto Tatsuta (Tohoku U.) 12:20 LUNCH 13:30 INVITED TALK 2 Adding proof objects and inductive definition mechanisms to Frege structures Masahiko Sato (Tohoku U.) 14:20 BREAK 14:50-15:50 SESSION 2 14:50 From term models to domains Wesley Phoa (Cambridge U.) 15:20 An abstract interpretation of ML equality kinds Carl A. Gunter (U. Pennsylvania) Elsa L. Gunter, David B. MacQueen (AT&T Bell Laboratories) 15:50 BREAK 16:20-17:10 INVITED TALK 3 Full abstraction and the context lemma Albert R. Meyer (MIT Laboratory for Computer Science) 19:00-20:30 RECEPTION at Sendai Tokyu Hotel WEDNESDAY 25 SEPTEMBER 9:30-11:00 SESSION 3 9:30 An efficiency preorder for processes S. Arun-Kumar (Indian Institute of Technology) M. Hennessy (U. Sussex) 10:00 On nets, algebras and modularity Alexander Rabinovich (IBM T.J. Watson Research Center) Boris A. Trakhtenbrot (MIT and Tel Aviv U.) 10:30 Towards a complete hierarchy of compositional dataflow models Bengt Jonsson (Swedish Institute of Computer Science) Joost N. Kok (Utrecht U.) 11:00 BREAK 11:30 INVITED TALK 4 Constructive aspects of classical logics Robert L. Constable (Cornell U.) 12:20 LUNCH 13:30 INVITED TALK 5 Applying formal methods to software development--partially Amir Pnueli (Weizmann Institute of Science) 14:20 BREAK 14:50-15:50 SESSION 4 14:50 Proving termination of general Prolog programs Krzysztof R. Apt (CWI, Amsterdam) Dino Pedreschi (U. Pisa) 15:20 On abstraction and the expressive power of programming languages John C. Mitchell (Stanford U.) 15:50 BREAK 16:20-17:10 INVITED TALK 6 Role of logic programming in the FGCS project Kazuhiro Fuchi (ICOT, Tokyo) 19:00-21:00 BANQUET at Sendai Tokyu Hotel Banquet Speech by Rod Burstall (Edinburgh U.) THURSDAY 26 SEPTEMBER 9:30-11:00 SESSION 5 9:30 Authentication and delegation with smart-cards M. Abadi, M. Burrows, C. Kaufman, B. Lampson (DEC Systems Research Center, Palo Alto) 10:00 Data flow analysis as model checking Bernhard Steffen (RWTH--Aachen) 10:30 On the adequacy of dependence-based representations for programs with heaps Phil Pfeiffer (U. Wisconsin-Madison) Rebecca Parsons Selke (Rice U.) 11:00 BREAK 11:30 INVITED TALK 7 From programming-by-example to proving-by-example Masami Hagiya (Kyoto U.) 12:20 LUNCH 13:30 INVITED TALK 8 Programming with constraints Jean-Louis Lassez (IBM Watson Research Center) 14:20 BREAK 14:50-16:05 SESSION 6 14:50 Polynomial recursion analysis in Pascal like programs Dieter Armbruster (U. Stuttgart) 15:05 Complexity of proving program correctness Hardi Hungar (U. Oldenburg) 15:20 Some normalization properties of Martin-Lof's type theory, and applications David Basin (Edinburgh U.) Doug Howe (Cornell U.) 15:35 Parametricity of extensionally collapsed term models of polymorphism and their categorical properties Ryu Hasegawa (Kyoto U.) 15:50 Programs with continuations and linear logic Shin-ya Nishizaki (Kyoto U.) 16:05 BREAK 16:35-17:35 SESSION 7 16:35 PI-calculus semantics of object-oriented programming languages David Walker (U. Technology, Sydney) 16:50 Wrapper semantics of an object oriented programming language with state Andreas V. Hense (U. Saarlandes, Saarbrucken) 17:05 Sharing actions and attributes in modal action logic Mark Ryan, Jose Fiadeiro, Tom Maibaum (Imperial College, London) 17:20 First order data types and first order logic Ralf Treinen (U. Saarlandes, Saarbrucken) 17:35 BREAK WITH SANDWICH 19:00-20:30 EVENING SESSION 8 Demos and informal presentations FRIDAY 27 SEPTEMBER 9:30-11:00 SESSION 9 9:30 Principal type-schemes of BCI-lambda-terms Sachio Hirokawa (Kyushu U.) 10:00 Intersection and union types F. Barbanera, M. Dezani-Ciancaglini (U. Torino) 10:30 The coherence of languages with intersection types John C. Reynolds (Carnegie Mellon U.) 11:00 BREAK 11:30 INVITED TALK 9 Singleton, union and intersection types in program extraction Susumu Hayashi (Ryukoku U.) 12:20 LUNCH BREAK 13:30-14:30 SESSION 10 13:30 Subtyping + extensionality: confluence of beta-eta reduction in F_(<=) Pierre-Louis Curien (LIENS/CNRS, Paris) Giorgio Ghelli (U. Pisa) 14:00 An extension of system F with subtyping Luca Cardelli (DEC Systems Research Center, Palo Alto) Simone Martini (U. Pisa) John C. Mitchell (Stanford U.) Andre Scedrov (U. Pennsylvania) 14:30 BREAK 15:00 INVITED TALK 10 Will logicians be replaced by machines? Dana S. Scott (Carnegie-Mellon U.) 15:50-16:00 CLOSING SESSION Albert R. Meyer, TACS Co-Chair (MIT) Takayasu Ito, TACS Co-Chair (Tohoku U.) SATURDAY 28 SEPTEMBER Bus Tour to Hiraizumi and Matsushima 9:00 Depart Sendai Tokyu Hotel Hiraizumi (Chusonji Temple with Golden Pavilion) Lunch Matsushima (Famous Views of Pine-covered Islets, Zuiganji Temple) Dinner at a Japanese restaurant 20:30 Return Sendai Tokyu Hotel -------------------------------------------------------------------------- GENERAL INFORMATION TACS'91 will be held on the campus of Tohoku University, Sendai, Japan. Lectures will be presented in the Aoba Memorial Building, Faculty of Engineering located on the Aoba Hill about 3 km west of downtown Sendai. Receptions and a banquet will be held at the Sendai Tokyu Hotel, located in downtown Sendai. A post conference bus tour to Hiraizuki (Chusonji Temple with its golden pavilion) and Matsushima (famous views of pine-covered islets and Zuiganji Temple) will take place on September 28. Sendai is the largest city in the northern part of the Honshu Island of Japan, with a population of about 900,000. The city is known in Japan as the "City of Trees". It is 350 km north from Tokyo and less than 2 hours away by the Tohoku Bullet Train (Tohoku Shinkansen). Sendai is a modern, safe city with a temperate climate blessed by four distinct, beautiful seasons. Conference registration is open to the public. Reservations for the post conference bus tour will be limited. Register and make reservations by returning the completed form below by email, FAX, or airmail. There will also be on-site registration at: Sendai Tokyu Hotel, 15:00-20:00, September 23, Aoba Memorial Bldg., Tohoku Univ., 9:00-17:00 on September 24-27. A proceedings, published as a volume in Springer-Verlag's Lecture Notes in Computer Science, will be given to registrants on arrival. TRANSPORTATION Conference participants arriving at the new TOKYO INTERNATIONAL (NARITA) Airport are advised to take the JR Narita Express train from Narita Airport to Tokyo Station. Then take the Yamabiko super express train of Tohoku Shinkansen (Tohoku Bullet Train) to Sendai from Tokyo. The Yamabiko runs almost every 30 min. and takes less than 2 hours from Tokyo to Sendai. Making reservations at Narita Station for the Yamabiko express is strongly recommended, since it will be the autumnal tourist season. NOTE: No flight service is available from Narita Airport to Sendai Airport, since the train service is superior. The JR Narita Express is a new service started this March, and Tohoku Shinkansen from Tokyo Station is a new service starting at the end of this June. If you are going to travel in Japan before/after the conference it will be convenient and economical to get a JR PASS before your departure. Contact your travel agent for more information. Those arriving at OSAKA INTERNATIONAL Airport can fly to Sendai Airport, and take the Limousine Bus service to Sendai Station. The bus takes about 45 min. to go from the Airport to Sendai Station. You can also take the Tokaido Shinkansen from Osaka to Tokyo Station and change at Tokyo Station to Tohoku Shinkansen for Sendai. Three recommended hotels offer special discount rates to TACS'91 participants: the Sendai Tokyu Hotel, the Sendai Washington Hotel II, and the Sendai Fuji Hotel. They are 1.2 km west of Sendai Station and about 500 Yen by taxi from the station. The receptions and banquet will be held at the Sendai Tokyu Hotel. The other two hotels are located within 5 min. walk of the Sendai Tokyu. CLIMATE The weather in Sendai from the middle of September to the middle of October is usually delightful--mostly sunny with temperatures ranging from the low 50's F (10's C) to the low 70's F (20's C). A light jacket may be needed in the morning and evening. Rain, if any, would rarely be heavy.