- -

Proving Operational Termination of Declarative Programs in General Logics

RiuNet: Institutional repository of the Polithecnic University of Valencia

Share/Send to

Cited by

Statistics

Proving Operational Termination of Declarative Programs in General Logics

Show full item record

Lucas Alba, S.; Meseguer, J. (2014). Proving Operational Termination of Declarative Programs in General Logics. ACM. doi:10.1145/2643135.2643152

Por favor, use este identificador para citar o enlazar este ítem: http://hdl.handle.net/10251/70132

Files in this item

Item Metadata

Title: Proving Operational Termination of Declarative Programs in General Logics
Author:
UPV Unit: Universitat Politècnica de València. Departamento de Sistemas Informáticos y Computación - Departament de Sistemes Informàtics i Computació
Issued date:
Abstract:
A declarative program P is a *theory* in a given computational logic L, so that *computation* with such a program is efficiently implemented as *deduction* in L. That is why *inference systems* are crucial: they both (i) ...[+]
Subjects: General Logics , Declarative Languages , Operational Termination , Program Verification
Copyrigths: Cerrado
ISBN: 978-1-4503-2947-7
DOI: 10.1145/2643135.2643152
Publisher:
ACM
Publisher version: http://dl.acm.org/citation.cfm?id=2643152&CFID=818641691&CFTOKEN=64363415
Conference name: 16th International Symposium on Principles and Practice of Declarative Programming (PPDP 2014)
Conference place: Canterbury, UK
Conference date: September 8-10, 2014
Type: Comunicación en congreso

References

P. Aczel. Schematic Consequence. In D. Gabbay, editor, What is a Logical System, pages 261--272, Oxford University Press, 1994.

B. Alarcón, F. Emmes, C. Fuhs, J. Giesl, R. Gutiérrez, S. Lucas, P. Schneider-Kamp, and R. Thiemann. Improving Context-Sensitive Dependency Pairs. In Proc. of LPAR'08, LNCS 5330:636--651, 2008.

B. Alarcón, S. Lucas, and J. Meseguer. A Dependency Pair Framework for A∨C-Termination. In Proc. of WRLA'10, LNCS 6381:35--51, 2010. [+]
P. Aczel. Schematic Consequence. In D. Gabbay, editor, What is a Logical System, pages 261--272, Oxford University Press, 1994.

B. Alarcón, F. Emmes, C. Fuhs, J. Giesl, R. Gutiérrez, S. Lucas, P. Schneider-Kamp, and R. Thiemann. Improving Context-Sensitive Dependency Pairs. In Proc. of LPAR'08, LNCS 5330:636--651, 2008.

B. Alarcón, S. Lucas, and J. Meseguer. A Dependency Pair Framework for A∨C-Termination. In Proc. of WRLA'10, LNCS 6381:35--51, 2010.

H.P. Barendregt, W. Dekkers, and R. Statman. Lambda Calculus with Types. Cambridge University Press, 2013.

M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and C. Talcott. All About Maude -- A High-Performance Logical Framework, LNCS volume 4350, 2007.

M. Codish and C. Taboch. A semantic basis for the termination analysis of logic programs. Journal of Logic Programming 41:103--123, 1999.

N. Dershowitz, N. Lindenstrauss, Y. Sagiv, and A. Serebrenik. A General Framework for Automatic Termination of Logic Programs. Applicable Algebra in Engineering, Communication and Computing, 12:117--156, 2001.

N. Dershowitz and Z. Manna. Proving Termination with Multiset Orderings. Communications of the ACM 22(8):465--476, 1979.

F. Durán, S. Lucas, J. Meseguer, C. Marché, and X. Urbain. Proving Termination of Membership Equational Programs. In Proc. of PEPM'04, pages 147--158, ACM Press, New York, 2004.

F. Durán, S. Lucas, C. Marché, J. Meseguer, X. Urbain, Proving Operational Termination of Membership Equational Programs, Higher-Order and Symbolic Computation 21(1-2):59--88, 2008.

F. Durán, S. Lucas, J. Meseguer. Methods for Proving Termination of Rewriting-based Programming Languages by Transformation. Electronic Notes in Theoretical Computer Science, 248:93--113, 2009.

F. Durán, S. Lucas, and J. Meseguer. MTT: The Maude Termination Tool (System Description). Proc. of IJCAR'08. LNAI 5195:313--319, 2008.

S. Falke and D. Kapur. Dependency Pairs for Rewriting with Built-in Numbers and Semantic Data Structures. In Proc. of RTA'08, LNCS 5117:94--109, 2008.

J. Giesl and D. Kapur. Dependency Pairs for Equational Rewriting. Proc. of RTA'01, LNCS 2051:93--108, 2001.

J. Giesl, R. Thiemann, and P. Schneider-Kamp. The Dependency Pair Framework: Combining Techniques for Automated Termination Proofs. In Proc. of LPAR'04, LNAI 3452:301--331, 2004.

J. Giesl, R. Thiemann, P. Schneider-Kamp, and S. Falke. Mechanizing and Improving Dependency Pairs. Journal of Automatic Reasoning, 37(3):155--203, 2006.

R. Gutiérrez and S. Lucas. Proving Termination in the Context-Sensitive Depedency Pairs Framework. In Proc of WRLA'10 LNCS 6381:19--35, 2010.

S. Lucas. Context-sensitive computations in functional and functional logic programs. Journal of Functional and Logic Programming, 1998(1):1--61, January 1998.

S. Lucas. Context-sensitive rewriting strategies. Information and Computation, 178(1):294--343, 2002.

S. Lucas and J. Meseguer. 2D Dependency Pairs for Proving Operational Termination of CTRSs. In Proc. of WRLA'14, LNCS vol. 8663, to appear, 2014.

S. Lucas and J. Meseguer. Order-Sorted Dependency Pairs. In Proc. of PPDP'08, pages 108--119, ACM Press, 2008.

S. Lucas, C. Marché, and J. Meseguer. Operational termination of conditional term rewriting systems. Information Processing Letters, 95:446--453, 2005.

J. Meseguer. General Logics. In H.-D. Ebbinghaus et al., editors, Logic Colloquium'87, pages 275--329, North-Holland, 1989.

J. Meseguer. Membership algebra as a logical framework for equational specification. In Proc. of WADT'97, LNCS 1376:18--61, 1998.

M. Nakamura, K. Ogata, and K. Futatsugi. On Proving Operational Termination Incrementally with Modular Conditional Dependency Pairs. International Journal of Computer Science, 40:2, 2013.

M.T. Nguyen, J. Giesl, P. Schneider-Kamp, and D. De Schreye. Termination Analysis of Logic Programs Based on Dependency Graphs. In Proc. of LOPSTR 2007, LNCS 4915:8--22, 2007.

E. Ohlebusch. Advanced Topics in Term Rewriting. Springer-Verlag, 2002.

F. Schernhammer and B. Gramlich. Characterizing and proving operational termination of deterministic conditional term rewriting systems. Journal of Logic and Algebraic Programming 79:659--688, 2010.

D. de Scheye and S. Decorte. Termination of Logic Programs: The Never-Ending Story. Journal of Logic Programming, 19:199--260, 1994.

P. Schneider-Kamp, J. Giesl, and M.T. Nguyen. The Dependency Triple Framework for Termination of Logic Programs. In Proc. of LOPSTR 2009, LNCS 6037:37--51, 2009.

[-]

This item appears in the following Collection(s)

Show full item record