TY  - UNPD
A1  - Panitz, Sven Eric
T1  - Termination proofs for a lazy functional language by abstract reduction : (draft)
T2  - Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik ; 6
N2  - Automatic termination proofs of functional programming languages are an often challenged problem Most work in this area is done on strict languages Orderings for arguments of recursive calls are generated In lazily evaluated languages arguments for functions are not necessarily evaluated to a normal form It is not a trivial task to de ne orderings on expressions that are not in normal form or that do not even have a normal form We propose a method based on an abstract reduction process that reduces up to the point when su cient ordering relations can be found The proposed method is able to nd termination proofs for lazily evaluated programs that involve non terminating subexpressions Analysis is performed on a higher order polymorphic typed language and termi nation of higher order functions can be proved too The calculus can be used to derive information on a wide range on di erent notions of termination.
T3  - Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik - 6 
Y1  - 1996
UR  - http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/4600
UR  - https://nbn-resolving.org/urn:nbn:de:hebis:30-8938
UR  - http://www.ki.informatik.uni-frankfurt.de/papers/panitz/term.ps
PB  - Johann Wolfgang Goethe-Univ., Fachbereich Informatik und Mathematik, Inst. für Informatik, Research group for Artificial Intelligence and Software Technology
CY  - Frankfurt [am Main]
ER  -