外山研輪講 紹介論文一覧 (2004年度)

• 2/23(水), 3/2(水) 紹介者: 駒木
  Hubert Comon,
  Completion of Rewrite Systems with Membership Constraints,
  Part I: Deduction Rules,
  J. Symbolic Computation. 25(4): 397-419 (1998).
• 1/26(水), 2/2(水) 紹介者: 後藤
  RON CYTRON, JEANNE FERRANTE, BARRY K.ROSEN & MARK N.WEGMAN, F KENNETH ZADECK,
  Efficiently Computing Static Single Assignment Form and the Control Dependence Graph,
  ACM Transactions on Programming Languages and Systems, Vol.13, No.4,
  October,1991,Pages 451-490.
• 12/8(水) 紹介者: 徳橋
  T.Genet, F.Klay.
  Rewriting for cryptographic protocol verification.
  In Proceedings of 17th International Conference on Automated Deduction,
  LNAI 1831, Springer-Verlag, pp.271-290, 2000.
• 12/8(水) 紹介者: 小滝
  W.-N.Chin.
  Towards an automated tupling strategy.
  In Proceedings of 3rd ACM Symposium on Partial Evaluation and
  Semantic-Based Program Manipulation, ACM Press, pp.119-132, 1993.
• 12/8(水) 紹介者: 瀬古
  T.Arts, J.Giesl.
  Termination of term rewriting using dependency pairs.
  Theoretical Computer Science 236(1-2), pp.133-178, 2000.
• 12/1(水) 紹介者: 青戸
  G. Huet and J.-J.L{\'e}vy.
  Computations in orthogonal term rewriting systems, I.
  In Computational Logic, Essays in Honour of J. Alan Robinson,
  pages 395-414. The MIT Press, 1992.
• 11/10(水), 11/17(水) 紹介者: 駒木
  Leo Bachmair and Nachum Dershowitz,
  Equational Inference, Canonical Proofs,and Proof Orderings,
  Journal of ACM 41(2), pp.236-276, 1994.
• 10/27(水) 紹介者: 外山
  G. D. Plotkin,
  Call-by-name, call-by-value and the lambda-calculus,
  Theoretical Computer Science, 1(2):125-159, December 1975.
• 10/20(水) 紹介者:菊池
  Silvio Valentini,
  An Elementary Proof of Strong Normalization for Intersection Types,
  Archive for Mathematical Logic, Vol.40, No.7, pp.475-488, 2001.
• 9/22(水), 7/30(木), 10/6(水), 10/13(水) 紹介者: 後藤
  Atsushi Ohori,
  A Polymorphic Record Calculus and Its Compilation,
  ACM Transactions on Programming Languages and Systems
  vol 17, no 6, pages 844-895, 1995.
• 6/30(水), 7/6(水), 7/14(水), 7/28(水) 紹介者: 千葉
  A. Compagnoni,
  Higher-order subtyping and its decidability,
  Information and Computation 191 (2004) 41-103.
• 6/23(水) 紹介者: 落合
  J. Giesl, R. Thiemann, P. Schneider-Kamp, and S. Falke,
  Improving Dependency Pairs,
  Thechnical Report AIB-2003-4, RWTH Aachen, May, 2003.
• 6/16(水) 紹介者: 坂本
  A. Bundy, A. Stevens, F. van Harmelen, A. Ireland, and A. Smaill,
  Rippling: a heuristic for guiding inductive proofs,
  Artificial Intelligence 62, pp.185-253, 1993.
• 5/26(水) 紹介者: 駒木
  Rolf Hennicker,
  Context Induction: A Proof Principle for Behavioural Abstractions and Algebraic Implementations,
  Formal Aspects of Computing 3(4):326-345,1991.
• 5/12(水) 紹介者: 青戸
  T.Aoto, T.Yamada and Y.Toyama,
  Inductive theorems for higher-order rewriting,
  In Proceedings of the 15th International Conference on Rewriting Techniques and Applications (RTA 2004), Aachen, Germany,
  Lecture Notes in Computer Science, Vol.3091, Springer-Verlag, pp.269-284, 2004.
• 4/14(水) 紹介者: 外山
  Y.Toyama,
  Termination of S-expression rewriting systems:
  Lexicographic path ordering for higher-order terms,
  In Proceedings of the 15th International Conference on Rewriting Techniques and Applications (RTA 2004), Aachen, Germany,
  Lecture Notes in Computer Science, Vol.3091, Springer-Verlag, pp.40-54, 2004.

webmaster