Date: Fri, 04 Nov 2005 12:07:22 -0700
From: Manuel Hermenegildo <herme@fi.upm.es>
Subject: Re: [curry] formal verification for functional-logic programming
	languages
In-reply-to: <200511041349.31920.wolfgang@jeltsch.net>
To: Wolfgang Jeltsch <wolfgang@jeltsch.net>
Cc: Curry ML <curry@informatik.rwth-aachen.de>
Reply-to: Manuel Hermenegildo <herme@fi.upm.es>
Message-id: <17259.45418.371166.231402@localhost.localdomain>
MIME-version: 1.0
Content-type: text/plain;
  charset=iso-8859-1
Content-transfer-encoding: 7bit
References: <200511041349.31920.wolfgang@jeltsch.net>


Hi Wolfgang,

 > where can I find information about formal verification techniques and tools 
 > for functional-logic programming languages?  Both introductionary texts and 
 > current research papers etc. are welcome.

Ciao (which is also a logic-functional programming language) includes
a verifying compiler, CiaoPP, which integrates many formal
verification techniques and tools (generally based on abstract
interpretation). I send you two pointers to tutorial introductions to
this work:

@inproceedings{ciaopp-sas03,
  author =       {M.~Hermenegildo and G.~Puebla and F.~Bueno
                  and P.~L\'{o}pez-Garc\'{\i}a}, 
  title =        {{P}rogram {D}evelopment {U}sing {A}bstract {I}nterpretation
                  (and {T}he {C}iao {S}ystem {P}reprocessor)},
  booktitle =    {10th {I}nternational {S}tatic {A}nalysis {S}ymposium 
                  (SAS'03)}, 
  year =         {2003},
  month =        {June},
  pages =        {127--152},
  number =       {2694},
  publisher =    {Springer-Verlag},
  publisher_location ={Heidelberg, Germany},
  series =       {LNCS}
}

http://www.cliplab.org/papers/ciaopp-sas03.pdf

@inproceedings{acc-res-ppdp05,
 author =       {M.~Hermenegildo and E.~Albert and
                 P.~L\'{o}pez-Garc\'{\i}a and G.~Puebla}, 
 title =        {{A}bstraction {C}arrying {C}ode and {R}esource-{A}wareness},
 booktitle =    {Proc. of 7th ACM-SIGPLAN International Symposium on
                 Principles and Practice of Declarative Programming (PPDP'05)},
 year =         {2005},
 month =        {July},
 publisher = 	{ACM Press},
 npages =       {11}
} 

http://www.cliplab.org/papers/acc-res-ppdp05.pdf
 
Hope this helps,

Manuel

-- 
-------------------------------------------------------------------------------
 herme@fi.upm.es                      |                    Manuel Hermenegildo
 +34-91-336-7435 (Work)               |                Facultad de Informatica
 +34-91-352-4819 or 336-7412 (FAX)    |      Universidad Politecnica de Madrid
 http://www.clip.dia.fi.upm.es/~herme | 28660-Boadilla del Monte, MADRID SPAIN
-------------------------------------------------------------------------------