{"entities":{"Q40287":{"pageid":40343,"ns":120,"title":"Item:Q40287","lastrevid":105428165,"modified":"2026-10-09T10:09:12Z","type":"item","id":"Q40287","labels":{"en":{"language":"en","value":"Psi-calculi"}},"descriptions":{"en":{"language":"en","value":"AFP entry Psi_Calculi"}},"aliases":{},"claims":{"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"812b562c59bb97ac3ace1ed43f192888af293cdf","datavalue":{"value":"28573","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40287$75A9993D-291A-4875-89E3-2108ECB6E31D","rank":"normal"}],"P286":[{"mainsnak":{"snaktype":"value","property":"P286","hash":"f2ce3f377c45a206dd446d2b8447b6caa83e105b","datavalue":{"value":{"entity-type":"item","numeric-id":5890661,"id":"Q5890661"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40287$FD22E95C-274E-458F-81DB-BF11D94C5A96","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":"Q40287$85DED464-A9B3-4E8D-A050-83A6FEC3D173","rank":"normal"}],"P29":[{"mainsnak":{"snaktype":"value","property":"P29","hash":"214fe795f63f74073eb74b58e6b1967353537d76","datavalue":{"value":"https://www.isa-afp.org/entries/Psi_Calculi.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40287$30372002-09E2-429A-AAD2-93DE7A8E8AB9","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"0db99c3b17fc587dc6d0b047e5ff5ce0de1786ab","datavalue":{"value":"03","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40287$CA8480C9-D3BC-4FAE-96A4-552F02EC5843","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"acf10290b955a69659a681d98822944f91bbad9e","datavalue":{"value":"68","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40287$D43AEBAF-B683-4A09-A19B-909C7E70E949","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"9ccfc2ffdb7a60cd36d8dca0a4e6d9d45f5228f3","datavalue":{"value":"3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40287$B464F4B0-7030-41C2-B8A6-6D74AD04E431","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"09f5e0c6033338f59ef27e37d6877da0f26d9646","datavalue":{"value":"68.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40287$DF599FD4-5E99-446B-9A96-9F0A51C547EE","rank":"normal"}],"P1458":[{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a2a767ccd0e9bdc5b1b4a2069a6679f9340a857a","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40287$759DAA9E-C27B-4D7E-8314-C7B80940AAA0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"acf5d0da134f7563af94342a3a34b9ca28cd59db","datavalue":{"value":{"entity-type":"item","numeric-id":23989,"id":"Q23989"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40287$5FFE4692-6C9B-4489-BD2C-DE04495CF29C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ecda3e6d8e971c0b93d4cf3afb41990e853f830f","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40287$055857F0-AF0D-4C6C-AB21-F32DD8AAB7EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"4244bd21b3a60c5b7dc07ce4b342a92594fee47f","datavalue":{"value":{"entity-type":"item","numeric-id":18957,"id":"Q18957"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40287$C71FD623-71B0-4C6B-B1D9-2FA5505515B0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"bc38458efffcff78fafbe01cd7c86606976b2c00","datavalue":{"value":{"entity-type":"item","numeric-id":13181,"id":"Q13181"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40287$131562CC-DD04-4FE6-86AF-FA42EE61C4AF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"cb15924b3f11a91ed3d52d01ae18199742cf1a39","datavalue":{"value":{"entity-type":"item","numeric-id":22078,"id":"Q22078"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40287$B32D2F10-DD64-4A7D-866D-A91F909661E3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"cc41d9364226bfa8139f8dbc43b1b77967245f13","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40287$7ACAF269-2E61-4F17-B1AB-C5D34EC90954","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"54967cdfff4fe27e4c75d99ed97c193e93bcbed1","datavalue":{"value":{"entity-type":"item","numeric-id":21444,"id":"Q21444"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40287$80904F5C-9230-4E9F-88C4-84FB3BAEC671","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"df2209f238bd09444b5840922237770a9a510d98","datavalue":{"value":{"entity-type":"item","numeric-id":14061,"id":"Q14061"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40287$76EB8113-2AE6-4C79-AEAA-8054ACF1CBB4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ed15eb8701a335444fde1bcc3327d1067ce64751","datavalue":{"value":{"entity-type":"item","numeric-id":24376,"id":"Q24376"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40287$B011D568-B604-4BEC-8A8B-1074CADD2933","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"bb05cb23794774f62a8e4aa4de610af231973a1d","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40287$05B2A72A-799D-4C1D-9E80-8D6B27845611","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"03281999c3208b8f3a62eaceadadf1ce834fe219","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40287$9E983B85-F0DC-458C-B7BA-E0D381394261","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"8dde418bf28e22fefe1976bd953eb7c8ec5b548d","datavalue":{"value":{"entity-type":"item","numeric-id":16770,"id":"Q16770"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40287$A01EB859-A3F0-4617-9465-63424DA37460","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"3d758980c7aab42229371c3fec56294874b60660","datavalue":{"value":{"entity-type":"item","numeric-id":22838,"id":"Q22838"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40287$6F38E9C5-6D59-4DCF-8F47-0F27DF012BC4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"cb1c6c5611d06e4e5633b0a5b6fa7e74cac6f46c","datavalue":{"value":{"entity-type":"item","numeric-id":26927,"id":"Q26927"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40287$C14335C2-3857-46CB-9F2D-46A459830E94","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"18e15e946a9b8db60c88d8c0a9a054a3d76ac633","datavalue":{"value":{"entity-type":"item","numeric-id":14553,"id":"Q14553"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40287$DF8698D6-1DF2-4A8D-AAE9-51D069F30EF7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a87e432b48d17ed223fc8f797ceda8d48d22986a","datavalue":{"value":{"entity-type":"item","numeric-id":22080,"id":"Q22080"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40287$67FB6301-2D7C-49C2-BE0F-9F945EEF276A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"7b93ae6ec78e58e28f961ea759e948bfede50fa2","datavalue":{"value":{"entity-type":"item","numeric-id":22079,"id":"Q22079"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40287$8AD56D8D-EB3B-4D60-B76A-5643F5E7D2D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"e3a4636b499ad73c6e1f6382fe110c6af887d381","datavalue":{"value":{"entity-type":"item","numeric-id":34404,"id":"Q34404"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40287$1DED4E9A-476B-4349-ABB1-5440D5FEA59F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"8533330b9fa0c1f7979d4af1d0e8bdba3ffc811c","datavalue":{"value":{"entity-type":"item","numeric-id":56651,"id":"Q56651"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40287$1A1EFDB2-AC48-4115-BCE3-A83075424DA3","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"1dfed1972573bfe94f9f7f1ef64d107e74b6277a","datavalue":{"value":"https://isa-afp.org/entries/Psi_Calculi.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40287$DFED3589-8120-4853-9BBD-A8B2E2B9B706","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"9bbc23ac69b29e1b298c949070882e0accbc9ff5","datavalue":{"value":"Jesper Bengtson","type":"string"},"datatype":"string"},"type":"statement","id":"Q40287$D3378E2B-04D0-4E57-A08C-CC6CC478C73F","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"ae95208fd61a48dd09b978f16aa7f4d61a41d938","datavalue":{"value":"Psi-calculi are extensions of the pi-calculus, accommodating arbitrary nominal datatypes to represent not only data but also communication channels, assertions and conditions, giving it an expressive power beyond the applied pi-calculus and the concurrent constraint pi-calculus. We have formalised psi-calculi in the interactive theorem prover Isabelle using its nominal datatype package. One distinctive feature is that the framework needs to treat binding sequences, as opposed to single binders, in an efficient way. While different methods for formalising single binder calculi have been proposed over the last decades, representations for such binding sequences are not very well explored. The main effort in the formalisation is to keep the machine checked proofs as close to their pen-and-paper counterparts as possible. This includes treating all binding sequences as atomic elements, and creating custom induction and inversion rules that to remove the bulk of manual alpha-conversions. This entry is described in detail in Bengtson's thesis .","type":"string"},"datatype":"string"},"type":"statement","id":"Q40287$5433EE7C-D82C-4F1A-9715-38AE166C393F","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"cb1b7ba883393415c2d36d90450052b088071aaa","datavalue":{"value":{"entity-type":"item","numeric-id":3395094,"id":"Q3395094"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40287$B3F2FCCF-BDCA-4256-B9DA-247CEE62F460","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"83518a77cd2dab248c96219fb02ab05b38a89c35","datavalue":{"value":{"entity-type":"item","numeric-id":2871830,"id":"Q2871830"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40287$F2713991-B6BC-4519-8BD5-07DF7A8912DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aab63358c2a9806af600f7f743907818a47bc22e","datavalue":{"value":{"entity-type":"item","numeric-id":5895110,"id":"Q5895110"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40287$D5E2FBD0-5530-47FF-B7B1-AE3EF33BFCF7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e032e5c6e8bfdc59b9877ebc9fd03a4c0f9bd0eb","datavalue":{"value":{"entity-type":"item","numeric-id":4897432,"id":"Q4897432"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40287$20A2AD13-499C-44CF-8167-7ADEDDC3FA04","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8c704d43a48e07ac24cfe13985bec3bdd1a17595","datavalue":{"value":{"entity-type":"item","numeric-id":834373,"id":"Q834373"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40287$03E11315-9AA6-4088-A1D4-6DEB2956FCEF","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"9d8047b677a36e307cc9bbb6b9315bc65a6f74ae","datavalue":{"value":{"time":"+2012-05-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":"Q40287$A08165D2-B03D-4ABB-ABEA-A6B0E25CB6F6","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"cbd73df20f766fc521bea59047067b5733073c33","datavalue":{"value":{"text":"Psi-calculi in Isabelle","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q40287$8B85E8BB-9255-4B97-A11E-51B91166DAEE","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":"Q40287$4B4BFDD7-DF6A-465D-BF3D-99FFAA176EF4","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"147d947971425f6e481a02787827e4705017a40a","datavalue":{"value":{"entity-type":"item","numeric-id":7360786,"id":"Q7360786"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40287$D74C5F1B-EA4D-45C6-9A6E-D490E1822DDB","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Psi-calculi","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Psi-calculi"}}}}}