Presentation 2015-01-26
Implementing a Conditional Dependency Pair Method for Proving Termination of Functional Programs with Exception Handling
Koichi OTA, Takeshi HAMAGUCHI, Masahiko SAKAI, Akihisa YAMADA, Naoki NISHIDA, Tohiki SAKABE,
PDF Download Page PDF download Page Link
Abstract(in Japanese) (See Japanese page)
Abstract(in English) In this paper, we discuss implementation of the conditional dependency pair method for proving termination of functional programs with exception handling. We show sufficient conditions for the unsatisfiability of constraints in dependency pairs, which is undecidable. More precisely, the conditions depend on the termination and confluence of the rewrite system which defines built-in functions. We incorporate our result into a termination prover NaTT for TRSs and show the usefulness of the method via experimental results.
Keyword(in Japanese) (See Japanese page)
Keyword(in English) functional program / exception handling / term rewriting system / termination
Paper # MSS2014-78,SS2014-42
Date of Issue

Conference Information
Committee MSS
Conference Date 2015/1/19(1days)
Place (in Japanese) (See Japanese page)
Place (in English)
Topics (in Japanese) (See Japanese page)
Topics (in English)
Chair
Vice Chair
Secretary
Assistant

Paper Information
Registration To Mathematical Systems Science and its applications(MSS)
Language JPN
Title (in Japanese) (See Japanese page)
Sub Title (in Japanese) (See Japanese page)
Title (in English) Implementing a Conditional Dependency Pair Method for Proving Termination of Functional Programs with Exception Handling
Sub Title (in English)
Keyword(1) functional program
Keyword(2) exception handling
Keyword(3) term rewriting system
Keyword(4) termination
1st Author's Name Koichi OTA
1st Author's Affiliation Graduate School of Information Science, Nagoya University()
2nd Author's Name Takeshi HAMAGUCHI
2nd Author's Affiliation Graduate School of Information Science, Nagoya University
3rd Author's Name Masahiko SAKAI
3rd Author's Affiliation Graduate School of Information Science, Nagoya University
4th Author's Name Akihisa YAMADA
4th Author's Affiliation Advanced Industrial Science and Technology
5th Author's Name Naoki NISHIDA
5th Author's Affiliation Graduate School of Information Science, Nagoya University
6th Author's Name Tohiki SAKABE
6th Author's Affiliation Graduate School of Information Science, Nagoya University
Date 2015-01-26
Paper # MSS2014-78,SS2014-42
Volume (vol) vol.114
Number (no) 415
Page pp.pp.-
#Pages 6
Date of Issue