{"entities":{"Q7361820":{"pageid":31520999,"ns":120,"title":"Item:Q7361820","lastrevid":105369689,"modified":"2026-10-07T13:38:37Z","type":"item","id":"Q7361820","labels":{"en":{"language":"en","value":"Strong Normalization of Moggis's Computational Metalanguage"}},"descriptions":{"en":{"language":"en","value":"AFP entry Lam-ml-Normalization"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"8e9556b863413b232e48ce7dbf10128596e7e9de","datavalue":{"value":"https://isa-afp.org/entries/Lam-ml-Normalization.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361820$FCD5747E-1AC7-4DE9-905C-0EC0549793DA","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b3d7c2ed1801c947497c606fa879c8b143f40729","datavalue":{"value":{"time":"+2010-08-29T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361820$D81BDD24-C742-4FC7-A775-01EADC682302","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"64750cb5148f8911e7b48f6f5354e1f7d54bd5da","datavalue":{"value":"Christian Doczkal","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361820$61C84C15-06A7-4BB9-BFC8-B7137EBCDBC9","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"3c331415813a6b6efa2d002099ce947d32c20d74","datavalue":{"value":{"text":"Strong Normalization of Moggis's Computational Metalanguage","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361820$5306E182-4D63-466D-AC12-B8267137E430","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"ce517d7e1bcbc98141f4c84d679dae75b645a3c5","datavalue":{"value":"Handling variable binding is one of the main difficulties in formal proofs. In this context, Moggi's computational metalanguage serves as an interesting case study. It features monadic types and a commuting conversion rule that rearranges the binding structure. Lindley and Stark have given an elegant proof of strong normalization for this calculus. The key construction in their proof is a notion of relational TT-lifting, using stacks of elimination contexts to obtain a Girard-Tait style logical relation. I give a formalization of their proof in Isabelle/HOL-Nominal with a particular emphasis on the treatment of bound variables.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361820$72A6C679-F500-4106-B5AC-0F89E0DE12F2","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"49ef7ea9ef7acf3b31e9421cfa44c2f14c047994","datavalue":{"value":{"entity-type":"item","numeric-id":2871835,"id":"Q2871835"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361820$9D551E1F-E8F5-4AE2-8C89-2A6C37909AE4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1851616a00610aaeabd4291b4d22573878184fd4","datavalue":{"value":{"entity-type":"item","numeric-id":3546313,"id":"Q3546313"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361820$42E4CA0F-A49B-46D6-82F5-489657D27F80","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3d8bfe191ca90d3395347096033dd0a0643030e0","datavalue":{"value":{"entity-type":"item","numeric-id":4281462,"id":"Q4281462"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361820$07214BF1-6040-4A95-B511-D16BDCEB627E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"42d924809cd7dde4fee01261ee91e6338b092ffe","datavalue":{"value":{"entity-type":"item","numeric-id":4236755,"id":"Q4236755"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361820$779D468A-177B-4C64-A005-78F5DD0B2574","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d8497b2d78ba0b1939b3cc4392136c45f636c16c","datavalue":{"value":{"entity-type":"item","numeric-id":817701,"id":"Q817701"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361820$25BD4741-9AD1-43B4-B55B-A220A8C09603","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"70d5dcacdf82491509f047ffa7adf630e71ade90","datavalue":{"value":{"entity-type":"item","numeric-id":5667469,"id":"Q5667469"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361820$2A68CA56-1943-49C4-B66D-53501289474C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cbed5b14a086787bebc35634de251ea7dadb5fb9","datavalue":{"value":{"entity-type":"item","numeric-id":4762953,"id":"Q4762953"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361820$68D2CD40-9147-4E57-8B9F-24EC406D413C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eed29b5bacdadf0aa4d60c6a8d9efaa13fa4ff36","datavalue":{"value":{"entity-type":"item","numeric-id":2871864,"id":"Q2871864"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361820$646D964C-D173-4292-AE5A-885795D359EC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"203af7b2224e70d9229da9b044eb4282ff6c7420","datavalue":{"value":{"entity-type":"item","numeric-id":3024835,"id":"Q3024835"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361820$CCDD2BC4-B3E1-4822-8C08-A33CC15A9B42","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"021e6e2184fd3d7f831680d56b426b95217eac7a","datavalue":{"value":{"entity-type":"item","numeric-id":4033837,"id":"Q4033837"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361820$B3F53322-65A1-43B9-BB8C-54379587E364","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1eb387d93d6d1c7b34f751c3ee7736c48adf0665","datavalue":{"value":{"entity-type":"item","numeric-id":1227601,"id":"Q1227601"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361820$7482EE44-9C68-4741-8E4B-1CC53D0E0CC3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"541bc36e9357802534d1e52134710ec758d76fb7","datavalue":{"value":{"entity-type":"item","numeric-id":5753923,"id":"Q5753923"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361820$3FA1E839-7DD3-4918-9FB2-5859D45B9E24","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1404903fbb3450c69ae4b46e148487834232fe43","datavalue":{"value":{"entity-type":"item","numeric-id":1823013,"id":"Q1823013"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361820$8C5E5C38-13E5-4C97-A42B-4876F8A107DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a10bbeb6c6903ace983b2dbf286a2ef4e5b248ab","datavalue":{"value":{"entity-type":"item","numeric-id":1331625,"id":"Q1331625"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361820$290F3279-7127-43E6-BBAC-8FA61B9F074B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5f01476c1579445ee6fcc8a24243fb3deb81fa48","datavalue":{"value":{"entity-type":"item","numeric-id":1450103,"id":"Q1450103"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361820$1E66DC80-E656-4B32-9F14-2C93216587C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"46ddc2d25595b2039aee78c8f5e062ccf7f85d04","datavalue":{"value":{"entity-type":"item","numeric-id":3543650,"id":"Q3543650"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361820$D4ADEC3A-1B93-4CBE-9508-1A1DF2FB8F93","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"79ce8544fc5a0489695eae9a558cb4d34b573281","datavalue":{"value":{"entity-type":"item","numeric-id":5477646,"id":"Q5477646"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361820$7C397B08-8098-47E3-AEBB-ABF3CDE8C70B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"99c6176bcb92cea3bde43c51d54f8875f446d09c","datavalue":{"value":{"entity-type":"item","numeric-id":3994895,"id":"Q3994895"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361820$B3430D25-9330-458E-8988-181B06476E0C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"91a707f7565046237d79754215ce6024facdf2b7","datavalue":{"value":{"entity-type":"item","numeric-id":4068054,"id":"Q4068054"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361820$784176C9-CD3B-4A74-B795-FAD67F731226","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"497b4c81f4eb1172c293c9383a73640c83e593d4","datavalue":{"value":{"entity-type":"item","numeric-id":4364399,"id":"Q4364399"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361820$F133D5BB-BA1C-48CD-822B-E2D2B230D828","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"486b3db15310f7b4419a518b9731479317d56d77","datavalue":{"value":{"entity-type":"item","numeric-id":1961921,"id":"Q1961921"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361820$7F3C1577-7E66-46E2-92BB-BE95C7334DD9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f66cc4b433a7230e47e5f58d1ea220d0e92f4725","datavalue":{"value":{"entity-type":"item","numeric-id":5704015,"id":"Q5704015"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361820$F0353232-1E72-4E5C-A153-98AADDB325AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"29dee98229347c3ff5d61b43b45d8e001f181167","datavalue":{"value":{"entity-type":"item","numeric-id":3608761,"id":"Q3608761"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361820$207B7F9A-BA84-4AC7-BE5E-68CD02F86CCE","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361820$17A44A9A-4A0F-4B4E-BB81-8527A8A0A834","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"bbbd01ab6fe9cda8df6fdce217eef2d86891f550","datavalue":{"value":{"entity-type":"item","numeric-id":7360795,"id":"Q7360795"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361820$206D28B9-030B-4755-B34D-ACE13AE41C1B","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361820$D04234B6-56B4-4B88-BB6A-E15D4FD473D3","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Strong Normalization of Moggis's Computational Metalanguage","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Strong_Normalization_of_Moggis%27s_Computational_Metalanguage"}}}}}