{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,24]],"date-time":"2025-03-24T06:51:06Z","timestamp":1742799066918},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540659228"},{"type":"electronic","value":"9783540488552"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/10703163_20","type":"book-chapter","created":{"date-parts":[[2006,10,9]],"date-time":"2006-10-09T14:15:50Z","timestamp":1160403350000},"page":"298-312","source":"Crossref","is-referenced-by-count":9,"title":["Monotone Fixed-Point Types and Strong Normalization"],"prefix":"10.1007","author":[{"given":"Ralph","family":"Matthes","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"20_CR1","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1109\/LICS.1996.561324","volume-title":"Proceedings of the Eleventh Annual IEEE Symposium on Logic in Computer Science","author":"M. Abadi","year":"1996","unstructured":"Abadi, M., Fiore, M.: Syntactic Considerations on Recursive Types. In: Proceedings of the Eleventh Annual IEEE Symposium on Logic in Computer Science, pp. 242\u2013252. IEEE Computer Society, Los Alamitos (1996)"},{"key":"20_CR2","unstructured":"Altenkirch, T.: Strong Normalization for T+. Unpublished note (1993)"},{"key":"20_CR3","first-page":"117","volume-title":"Handbook of Logic in Computer Science","author":"H. Barendregt","year":"1993","unstructured":"Barendregt, H.: Lambda Calculi with Types. In: Abramsky, S., Gabbay, D., Maibaum, T. (eds.) Handbook of Logic in Computer Science, vol.\u00a02, pp. 117\u2013309. Oxford Univ. Press, Oxford (1993)"},{"key":"20_CR4","unstructured":"Geuvers, H.: Inductive and Coinductive Types with Iteration and Recursion. In: Nordstr\u00f6m, B., Pettersson, K., Plotkin, G. (eds.) Preliminary Proceedings of the Workshop on Types for Proofs and Programs, B\u00e5stad, pp. 193\u2013217 (June 1992) (ftp:\/\/ftp.cs.chalmers.se\/pub\/cs-reports\/baastad.92\/proc.dvi.Z)"},{"key":"20_CR5","volume-title":"Proofs and Types","author":"J.-Y. Girard","year":"1989","unstructured":"Girard, J.-Y., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge Univ. Press, Cambridge (1989)"},{"key":"20_CR6","series-title":"Foundations of Computing Series","volume-title":"Semantics of Programming Languages: Structures and Techniques","author":"C.A. Gunter","year":"1992","unstructured":"Gunter, C.A.: Semantics of Programming Languages: Structures and Techniques. Foundations of Computing Series. The MIT Press, Cambridge (1992)"},{"key":"20_CR7","series-title":"APIC Studies in Data Processing","first-page":"279","volume-title":"Logic in Computer Science","author":"D. Leivant","year":"1990","unstructured":"Leivant, D.: Contracting Proofs to Programs. In: Odifreddi, P. (ed.) Logic in Computer Science. APIC Studies in Data Processing, vol.\u00a031, pp. 279\u2013327. Academic Press, London (1990)"},{"key":"20_CR8","unstructured":"Loader, R.: Normalisation by Translation. Unpublished note announced on the \u201ctypes\u201d mailing list on April 6 (1995)"},{"key":"20_CR9","unstructured":"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 \n                    \n                      http:\/\/www.tcs.informatik.uni-muenchen.de\/~matthes\/"},{"key":"20_CR10","first-page":"30","volume-title":"Proceedings of the Second Annual IEEE Symposium on Logic in Computer Science","author":"N.P. Mendler","year":"1987","unstructured":"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\u201336. IEEE Computer Society, Los Alamitos (1987)"},{"key":"20_CR11","unstructured":"van Raamsdonk, F., Severi, P.: On Normalisation. Technical Report CS-R9545, CWI (June 1995)"},{"key":"20_CR12","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1006\/inco.1995.1057","volume":"118","author":"M. Takahashi","year":"1995","unstructured":"Takahashi, M.: Parallel Reduction in \u03bb-Calculus. Information and Computation\u00a0118, 120\u2013127 (1995)","journal-title":"Information and Computation"},{"key":"20_CR13","unstructured":"Uustalu, T., Vene, V.: A Cube of Proof Systems for the Intuitionistic Predicate \u03bc-, \u03bd-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.\u00a0248, pp. 237\u2013246 (May 1997)"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10703163_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T15:29:42Z","timestamp":1558279782000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10703163_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540659228","9783540488552"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/10703163_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1999]]}}}