A termination proof of reduction in a simply typed calculus with constructors
The well-known proof of termination of reduction in simply typed calculi is adapted to a monomorphically typed lambda-calculus with case and constructors and recursive data types. The proof differs at several places from the standard proof. Perhaps it is useful and can be extended also to more complex calculi.
| Author: | Manfred Schmidt-Schauß, David Sabel |
|---|---|
| URN: | urn:nbn:de:hebis:30-115435 |
| URL: | http://www.ki.informatik.uni-frankfurt.de/papers/schauss/frank-42.pdf |
| Series (Serial Number) | Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik (42) |
| Publisher: | Johann Wolfgang Goethe-Univ., Fachbereich Informatik und Mathematik, Inst. für Informatik, Research group for Artificial Intelligence and Software Technology |
| Place of publication: | Frankfurt [am Main] |
| Document Type: | Working Paper |
| Language: | English |
| Date of Publication (online): | 15.09.2011 |
| Year of first Publication: | 2010 |
| Publishing Institution: | Univ.-Bibliothek Frankfurt am Main |
| HeBIS PPN: | 277084393 |
| Institutes: | Informatik |
| Dewey Decimal Classification: | 004 Datenverarbeitung; Informatik |
| Sammlungen: | Universitätspublikationen |
| Licence (German): |  Veröffentlichungsvertrag für Publikationen ohne Print on Demand |
