- -

Proving Operational Termination of Declarative Programs in General Logics

RiuNet: Repositorio Institucional de la Universidad Politécnica de Valencia

Compartir/Enviar a

Citas

Estadísticas

  • Estadisticas de Uso

Proving Operational Termination of Declarative Programs in General Logics

Mostrar el registro completo del ítem

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

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

Ficheros en el ítem

[Cerrado]
Nombre: p32.pdf
Tamaño: 426.2Kb
Formato: PDF
Descripción: Versión editorial
Solicitar una copia al autor

Metadatos del ítem

Título: Proving Operational Termination of Declarative Programs in General Logics
Autor: Lucas Alba, Salvador Meseguer, José
Entidad UPV: Universitat Politècnica de València. Departamento de Sistemas Informáticos y Computación - Departament de Sistemes Informàtics i Computació
Fecha difusión:
Resumen:
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) ...[+]
Palabras clave: General Logics , Declarative Languages , Operational Termination , Program Verification
Derechos de uso: Cerrado
ISBN: 978-1-4503-2947-7
DOI: 10.1145/2643135.2643152
Editorial:
ACM
Versión del editor: http://dl.acm.org/citation.cfm?id=2643152&CFID=818641691&CFTOKEN=64363415
Título del congreso: 16th International Symposium on Principles and Practice of Declarative Programming (PPDP 2014)
Lugar del congreso: Canterbury, UK
Fecha congreso: September 8-10, 2014
Código del Proyecto:
info:eu-repo/grantAgreement/NSF//1319109/US/TWC: Small: Collaborative: Extensible Symbolic Analysis Modulo SMT: Combining the Powers of Rewriting, Narrowing, and SMT Solving in Maude/
info:eu-repo/grantAgreement/MICINN//TIN2010-21062-C02-02/ES/SWEETLOGICS-UPV/
info:eu-repo/grantAgreement/MINECO//TIN2013-45732-C4-1-P/ES/UNA APROXIMACION DECLARATIVA AL MODELADO, ANALISIS Y RESOLUCION DE PROBLEMAS/
info:eu-repo/grantAgreement/GVA//BEST%2F2014%2F026/
info:eu-repo/grantAgreement/GVA//PROMETEO%2F2011%2F052/ES/LOGICEXTREME: TECNOLOGIA LOGICA Y SOFTWARE SEGURO/
Agradecimientos:
Partially supported by NSF grant CNS 13-19109. Salvador Lucas’ research was developed during a sabbatical year at the UIUC and was also supported by the EU (FEDER), Spanish MINECO projects TIN2010-21062-C02-02 and TIN ...[+]
Tipo: 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.

[-]

recommendations

 

Este ítem aparece en la(s) siguiente(s) colección(ones)

Mostrar el registro completo del ítem