{"entities":{"Q3582695":{"pageid":5612599,"ns":120,"title":"Item:Q3582695","lastrevid":51062549,"modified":"2026-01-16T11:13:35Z","type":"item","id":"Q3582695","labels":{"en":{"language":"en","value":"Structured formal development with quotient types in Isabelle/HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5774496"}},"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":"Q3582695$D55A4A4D-A3C1-4DAB-A2BD-5D2B8B434927","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"4c47dd17ba253e78274d8f1557527255f771bdef","datavalue":{"value":{"text":"Structured Formal Development with Quotient Types in Isabelle/HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3582695$A2D82253-B537-4336-A8F9-CD7961588B1B","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"75e3ea6f15f0bbd482a8d8d0589c844a4e42e212","datavalue":{"value":"1286.68391","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3582695$D8F9CF5A-76F6-4485-9790-1803A7B0B4CE","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"7cae35d83b27d140bbc43f474e93efdc758b9aad","datavalue":{"value":"10.1007/978-3-642-14128-7_5","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3582695$05B7A13C-E92D-4AAE-9125-F72C4B62ED4C","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"6884dcd553d8669c30774eb71f232565b4c5e680","datavalue":{"value":{"entity-type":"item","numeric-id":3431399,"id":"Q3431399"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3582695$A7F4236B-2D13-44C6-9D42-DC292E14C568","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ce00bf932e8d4142816bb1d3b66ef3457d10b848","datavalue":{"value":{"entity-type":"item","numeric-id":626932,"id":"Q626932"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3582695$10B18961-6915-4E76-B666-863FDCB2C6CD","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3582695$937A6A9C-F598-4A2F-99D5-0D5F7887B08A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"d01ea8a4f82b63cae0dd5c2ac5f8977df7e5fa52","datavalue":{"value":{"time":"+2010-08-24T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3582695$423E5B35-3B45-4615-83CF-D1A77312B480","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3582695$34A34B53-68E1-448C-A2E9-4F2ACF9583E8","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"48d4ee9aab953a14601d2fa96bfa84ce87935522","datavalue":{"value":"5774496","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3582695$A39BF96D-719D-4373-AECB-A41403B7F39A","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c5fcda2c98ddff866834785339eb37077e5eb1fe","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3582695$A16E16E2-7D9C-44D1-B0E0-38A0EDEB4E10","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3582695$93AE309A-1855-4C14-B0DB-F44EEC2E1FFE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"01712194c207617871fd4fb99ad1e9fcc6e71eb8","datavalue":{"value":{"entity-type":"item","numeric-id":15955,"id":"Q15955"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3582695$F60EC88F-BCD7-4A74-BAFC-3E9BC66DA813","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":"Q3582695$09017420-7B2C-427E-AA92-32CAA9C69E8A","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"afedfc447da12a51daa47d9e82ee96f789a040f5","datavalue":{"value":"https://doi.org/10.1007/978-3-642-14128-7_5","type":"string"},"datatype":"url"},"type":"statement","id":"Q3582695$F84F6D69-508D-4685-B6AD-3C7777667526","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"45d8178255e38ef48f5a8c4aa0f603a9849b30fa","datavalue":{"value":"W4255801913","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3582695$BA094248-5319-4416-A1CA-0F595B940567","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"66bb2ac79eb425e6d340ace0d3214e8a8bc2a028","datavalue":{"value":{"entity-type":"item","numeric-id":3431400,"id":"Q3431400"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"25f0fb258d283f1d4066d2fa2760b3ae2f922942","datavalue":{"value":{"amount":"+0.83269202709198","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":"Q3582695$3F42D0C2-89DE-441F-817B-5B100ECFB2A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1be9a2d1d45856fc234e9cf534d673080b14f031","datavalue":{"value":{"entity-type":"item","numeric-id":2938044,"id":"Q2938044"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c1f3c9f3d0cce316b5b79fc6be14b783a4fcad30","datavalue":{"value":{"amount":"+0.7945658564567566","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":"Q3582695$CA7827F8-1E25-4426-81E0-F65D5E2FFD4C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"441897fe7904c9e44fbfc08e8a7a55eaf5c3e772","datavalue":{"value":{"entity-type":"item","numeric-id":5392587,"id":"Q5392587"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f5f858fb3c92986d76da82fe0d1b3e0bae90b425","datavalue":{"value":{"amount":"+0.7547576427459717","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":"Q3582695$297ACBB3-8646-43E1-A2F6-A0B8C7A9A4D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d9116eb982bedd5bbcafeae133c985cc55f30d2f","datavalue":{"value":{"entity-type":"item","numeric-id":5477651,"id":"Q5477651"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"912452d1de46229a7df93505488f4deccddf6fac","datavalue":{"value":{"amount":"+0.7439695000648499","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":"Q3582695$38213D43-3246-4330-9B9B-44A206134AD1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6c013473e7b4cccdc138bb31021c66fd5349a7c5","datavalue":{"value":{"entity-type":"item","numeric-id":4944854,"id":"Q4944854"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e1657d5a898cd5e07b15b5e4819cf0dab70a8345","datavalue":{"value":{"amount":"+0.7364529967308044","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":"Q3582695$C3B251E3-D4E4-4ADA-8BDC-0FAC9371AB87","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3582695","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3582695"}}}}}