{"entities":{"Q1946673":{"pageid":1957415,"ns":120,"title":"Item:Q1946673","lastrevid":57612948,"modified":"2026-03-31T15:09:39Z","type":"item","id":"Q1946673","labels":{"en":{"language":"en","value":"The \\(\\lambda \\mu^{\\mathbf{T}}\\)-calculus"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6154067"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1946673$5152A0D4-8E5B-45AF-9275-FF9D667F95F6","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"8ecc52c71fd96fcdb40486fd13abd12fc7df370e","datavalue":{"value":{"text":"The \\(\\lambda \\mu^{\\mathbf{T}}\\)-calculus","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1946673$5623427C-C9EB-4B8D-9F9F-406EAD618823","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"37dd7254c4a79347c1469ccb944158f9fc14bc34","datavalue":{"value":"1273.03053","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1946673$C1895B58-BB70-4F6B-8E84-EC0C4A23871F","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"d617c217f8f04ef480d650a973c1ec01fe67123b","datavalue":{"value":{"entity-type":"item","numeric-id":235622,"id":"Q235622"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1946673$368204B5-B325-473E-99EE-357E38C61480","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"d784fe6cc5179886bfe36c86ddc8bdd92ade5a26","datavalue":{"value":{"entity-type":"item","numeric-id":549190,"id":"Q549190"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1946673$CB53BF43-DA9F-48B6-89C1-683675F82F16","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"d6d72c052d6a5ad7a719f388761353f23640a4e3","datavalue":{"value":{"entity-type":"item","numeric-id":1725925,"id":"Q1725925"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1946673$37B8F65A-8E99-42D6-9986-DF98DC710A0D","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f91a4bcbc93435aed71775d25a4c5cd09e26f12d","datavalue":{"value":{"entity-type":"item","numeric-id":122505,"id":"Q122505"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1946673$861AC043-4224-4F37-A169-192FAA7FE8E0","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"765cd593eb4c0a85f684310f1c77606d8c65d861","datavalue":{"value":{"time":"+2013-04-15T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1946673$2CC540BD-B50A-42EF-B07A-03CF92DD4F9A","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"ae62926be758bc6137b5883cc574dbf0b476f31e","datavalue":{"value":"https://arxiv.org/abs/1204.0347","type":"string"},"datatype":"url"},"type":"statement","id":"Q1946673$30C0BF1F-857B-4688-BDE2-09D178F2C7C7","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"8e3d408376ed90362394d6e7bd6de2b50b9dc290","datavalue":{"value":"The calculus \\(\\lambda\\mu^{\\mathbf{T}}\\), a combination of Parigot's \\(\\lambda\\mu\\)-calculus and G\u00f6del's \\textbf{T}, is introduced. The motivation is to provide a type-theoretic framework for challenge constructs in real programming languages, including datatypes such as the natural numbers, primitive recursion, and control operators such as catch and throw. In other words, the paper aims at a synthesis of classical computation with datatypes with a conventional metatheory of typing and reduction.  Meta-theoretical properties of \\(\\lambda\\mu^{\\mathbf{T}}\\), such as subject reduction, normal forms, confluence and strong normalization, are studied. For the proofs of the latter two properties some adaptations of known techniques from the literature are required. Moreover, it is shown that exactly the provably recursive functions in first-order arithmetic can be represented in \\(\\lambda\\mu^{\\mathbf{T}}\\).","type":"string"},"datatype":"string"},"type":"statement","id":"Q1946673$1CECE53D-40EF-4408-85E8-6490C0FB16FE","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"25aa969dcca62ee94c95b2a54e4102ee8a17d130","datavalue":{"value":"03B40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1946673$A0AE0911-FCCB-4332-8A4C-1BEEC190BB84","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"136db5bb8708e52501dec32644ab90fd42c4c538","datavalue":{"value":"68N18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1946673$6CF9D576-6201-4F1C-846F-393FFBA1EABA","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"89435db4602ac837f7b7acffbcf5d957f97e9897","datavalue":{"value":"6154067","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1946673$EA004FA5-B5E3-4393-89AC-6CAB499FFDF7","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4db7dd9c231ccc760998670a9221b24aa1e3ccd8","datavalue":{"value":"lambda-calculus with control","type":"string"},"datatype":"string"},"type":"statement","id":"Q1946673$5A5CF1E8-69BA-4237-999E-E26B17293650","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b38049d159af5d6c62de79db7ea882fef0c299bd","datavalue":{"value":"confluence","type":"string"},"datatype":"string"},"type":"statement","id":"Q1946673$430E6DB7-DE31-4708-94A1-4F7E89172C68","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"af462e56ed2ce88a42c8df0ec7f2dc6a55ded212","datavalue":{"value":"strong normalization","type":"string"},"datatype":"string"},"type":"statement","id":"Q1946673$5E883996-6C14-4FB7-8E0F-24BF0843154B","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1946673$0F32BDCF-E4BC-403A-B4E8-66AF773D773C","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"a60022d8b5f75f4a05f3dbbad49ab23b34c853b3","datavalue":{"value":"W1584499102","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1946673$AD504094-5299-41F0-BCF7-AA5AA772E1ED","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"9cb470a40fb6b4b92e9c2367cc294216a4fce154","datavalue":{"value":"10.1016/J.APAL.2012.05.005","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1946673$855DFA92-3C1D-4F21-80F6-9E3D695FAC07","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1e268013a2b619b7c21b2276357366cf3ebb236c","datavalue":{"value":{"entity-type":"item","numeric-id":4218109,"id":"Q4218109"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ce54e361786d21b1d1120e203acc13eacca60aaa","datavalue":{"value":{"amount":"+0.8327752947807312","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1946673$F686A95C-78AB-4A40-ABDF-71F3F53146E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"57f01918a548a806393a334af6e6e25fff258fb8","datavalue":{"value":{"entity-type":"item","numeric-id":4986734,"id":"Q4986734"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"627a6d31f5f741a810ee1d9527aa281ee35f3580","datavalue":{"value":{"amount":"+0.8008998036384583","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1946673$D54C8722-3628-44E4-B98D-05AF73826115","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"58cea95e93db7482ea77b2a79109715dd0655731","datavalue":{"value":{"entity-type":"item","numeric-id":4948005,"id":"Q4948005"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"55034af0596fd93fdaca26b5e9925dbc66e655f2","datavalue":{"value":{"amount":"+0.7971476912498474","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1946673$49386B4C-3294-4F05-A6E5-F683EE7D1D48","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"23009ce55f8277af134c1b6790070733fdb97bc0","datavalue":{"value":{"entity-type":"item","numeric-id":4583170,"id":"Q4583170"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2be76a16d15d45cd489bc090042f3808a1f8464e","datavalue":{"value":{"amount":"+0.7971010804176331","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1946673$6AE30148-5E62-43AE-90F3-EC04244D90F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1f0ab1edf7612c42a1357b64dd03cd97b5cca22e","datavalue":{"value":{"entity-type":"item","numeric-id":4236202,"id":"Q4236202"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bd932e7b4321d451a85f1de820bf65b4539f5cf1","datavalue":{"value":{"amount":"+0.7925684452056885","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1946673$9ADEAAB4-5B82-48F0-ABF3-F8D59BE2EE5E","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1946673","badges":[]}}}}}