{"entities":{"Q7361230":{"pageid":31519229,"ns":120,"title":"Item:Q7361230","lastrevid":105364196,"modified":"2026-10-07T13:35:15Z","type":"item","id":"Q7361230","labels":{"en":{"language":"en","value":"Locally Nameless Sigma Calculus"}},"descriptions":{"en":{"language":"en","value":"AFP entry Locally-Nameless-Sigma"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"8cc1c1059d6732a25024e22c8716831cc95a2dfc","datavalue":{"value":"https://isa-afp.org/entries/Locally-Nameless-Sigma.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361230$B49A215C-419F-4C77-9BDB-7EB14662BE6E","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"0d8f90caf8d1da2bf9b942666efc1ceba9ba6cb6","datavalue":{"value":{"time":"+2010-04-30T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361230$DDF44946-FC86-4C76-A512-AD6228038756","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"d83ac3a54430d51a92913947cf52abf7bc1711d6","datavalue":{"value":"Ludovic Henrio","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361230$E79D1CF7-40B9-4A94-8153-9ACD7B42CAD2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"550a62a4781d2221da3e1fe70015fe78140acf8b","datavalue":{"value":"Florian Kamm\u00fcller","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361230$BEFFB5CE-C057-4283-AF71-20A050A2E28E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"bef43e90928772a15dfaef9217e3b99d4beb4488","datavalue":{"value":"Bianca Lutz","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361230$4CB61ECC-EAAE-4AFA-95DA-F17DDBACEFA1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"5f863df4c259fdebe990968cc25796fe4601e06c","datavalue":{"value":"Henry Sudhof","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361230$940C2B66-BD12-4261-BA5A-DFCA23E52E7C","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"a7bc63146c30d6f80425eea594f4c9ce2632486c","datavalue":{"value":{"text":"Locally Nameless Sigma Calculus","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361230$46CB1B78-45D5-46EE-BD0B-FF8C85949C5D","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"28880f25bb6f7244d2b14a37a1836369060d824b","datavalue":{"value":"We present a Theory of Objects based on the original functional sigma-calculus by Abadi and Cardelli but with an additional parameter to methods. We prove confluence of the operational semantics following the outline of Nipkow's proof of confluence for the lambda-calculus reusing his theory Commutation, a generic diamond lemma reduction. We furthermore formalize a simple type system for our sigma-calculus including a proof of type safety. The entire development uses the concept of Locally Nameless representation for binders. We reuse an earlier proof of confluence for a simpler sigma-calculus based on de Bruijn indices and lists to represent objects.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361230$5B97D145-EBFF-40EB-837B-3381A9A532FF","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":"Q7361230$E61A5EDE-2203-4323-B3BD-868BAE08E4E5","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"8cf17faf422fed75969aa9ebe32b8797880978b1","datavalue":{"value":{"entity-type":"item","numeric-id":7361733,"id":"Q7361733"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361230$194AB8CD-4002-419A-8AF6-8F3478573FE6","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"9beb5f7be6b27e22c4af581585b828086bbf7950","datavalue":{"value":{"entity-type":"item","numeric-id":7360796,"id":"Q7360796"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361230$CCB8D29C-0D12-4ACE-90F5-F10CBBF20EE6","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":"Q7361230$17016B29-B5BF-4018-AB7B-E134D3AC7F26","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Locally Nameless Sigma Calculus","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Locally_Nameless_Sigma_Calculus"}}}}}