Abstract
Several systems of fixed-point types (also called retract types or recursive types with explicit isomorphisms) extending system F are considered. The seemingly strongest systems have monotonicity witnesses and use them in the definition of beta reduction for those types. A more naïve approach leads to non-normalizing terms. All the other systems are strongly normalizing because they embed in a reduction-preserving way into the system of non-interleaved positive fixed-point types which can be shown to be strongly normalizing by an easy extension of some proof of strong normalization for system F.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abadi, M., Fiore, M.: Syntactic Considerations on Recursive Types. In: Proceedings of the Eleventh Annual IEEE Symposium on Logic in Computer Science, pp. 242–252. IEEE Computer Society, Los Alamitos (1996)
Altenkirch, T.: Strong Normalization for T+. Unpublished note (1993)
Barendregt, H.: Lambda Calculi with Types. In: Abramsky, S., Gabbay, D., Maibaum, T. (eds.) Handbook of Logic in Computer Science, vol. 2, pp. 117–309. Oxford Univ. Press, Oxford (1993)
Geuvers, H.: Inductive and Coinductive Types with Iteration and Recursion. In: Nordström, B., Pettersson, K., Plotkin, G. (eds.) Preliminary Proceedings of the Workshop on Types for Proofs and Programs, Båstad, pp. 193–217 (June 1992) (ftp://ftp.cs.chalmers.se/pub/cs-reports/baastad.92/proc.dvi.Z)
Girard, J.-Y., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge Univ. Press, Cambridge (1989)
Gunter, C.A.: Semantics of Programming Languages: Structures and Techniques. Foundations of Computing Series. The MIT Press, Cambridge (1992)
Leivant, D.: Contracting Proofs to Programs. In: Odifreddi, P. (ed.) Logic in Computer Science. APIC Studies in Data Processing, vol. 31, pp. 279–327. Academic Press, London (1990)
Loader, R.: Normalisation by Translation. Unpublished note announced on the “types” mailing list on April 6 (1995)
Matthes, R.: Extensions of System F by Iteration and Primitive Recursion on Monotone Inductive Types. PhD thesis, University of Munich (1998), to appear, available via http://www.tcs.informatik.uni-muenchen.de/~matthes/
Mendler, N.P.: Recursive Types and Type Constraints in Second-Order Lambda Calculus. In: Proceedings of the Second Annual IEEE Symposium on Logic in Computer Science, pp. 30–36. IEEE Computer Society, Los Alamitos (1987)
van Raamsdonk, F., Severi, P.: On Normalisation. Technical Report CS-R9545, CWI (June 1995)
Takahashi, M.: Parallel Reduction in λ-Calculus. Information and Computation 118, 120–127 (1995)
Uustalu, T., Vene, V.: A Cube of Proof Systems for the Intuitionistic Predicate μ-, ν-Logic. In: Haveraaen, M., Owe, O. (eds.) Selected Papers of the 8th Nordic Workshop on Programming Theory (NWPT 1996), Oslo, Norway. Research Reports, Department of Informatics, University of Oslo, vol. 248, pp. 237–246 (May 1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Matthes, R. (1999). Monotone Fixed-Point Types and Strong Normalization. In: Gottlob, G., Grandjean, E., Seyr, K. (eds) Computer Science Logic. CSL 1998. Lecture Notes in Computer Science, vol 1584. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10703163_20
Download citation
DOI: https://doi.org/10.1007/10703163_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65922-8
Online ISBN: 978-3-540-48855-2
eBook Packages: Springer Book Archive