{"entities":{"Q1764432":{"pageid":1775174,"ns":120,"title":"Item:Q1764432","lastrevid":48422338,"modified":"2026-01-04T16:49:57Z","type":"item","id":"Q1764432","labels":{"en":{"language":"en","value":"Certifying circuits in type theory"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 2138509"}},"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":"Q1764432$08F8DAF1-9053-4A02-9B40-3E247670FD17","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"330a1666e7db9d37875852aefb79da0c87238490","datavalue":{"value":{"text":"Certifying circuits in type theory","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1764432$F313AD7F-5709-4DA1-AB28-1087B20E7592","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"21dc1acb8552eb794b0d46bafc5eb622dec57c72","datavalue":{"value":"1061.68105","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1764432$CF674902-B43E-4CC5-B463-871E34B9EC98","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"614d74f64afaae28ce84dfb41f91fb963f265197","datavalue":{"value":{"entity-type":"item","numeric-id":857882,"id":"Q857882"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1764432$F5B4CAC2-2F22-421E-A492-1D6F23693CA2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"e9bb03111d9adc852203f9f13bc23c3c7f55f605","datavalue":{"value":{"entity-type":"item","numeric-id":1764431,"id":"Q1764431"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1764432$F99CF20F-4AC7-4FE9-9151-FB240B3EE66B","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"d9925518446645d219093152a820aba790417b61","datavalue":{"value":{"entity-type":"item","numeric-id":164203,"id":"Q164203"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1764432$DF6C84D8-F59C-4A73-9F15-3DD198C64288","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"acb9018679bc717a3868823379e1b5aa1d36ccf9","datavalue":{"value":{"time":"+2005-02-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":"Q1764432$57C5DCBD-6A30-4855-AB30-4A721E3F4736","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"092d9a7dfbbaaa84ba458f8d83190fce94c9aa54","datavalue":{"value":"68Q65","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1764432$CBACE8E9-EE89-49F1-90F4-97AC5EC2DBB4","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"19fbd1ecca68bd77f4e8c280a56f159945f8fba3","datavalue":{"value":"2138509","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1764432$A5D0B59F-7833-40F1-8CB7-0D2CEB0143E6","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1b3f210910becb27540644b96d59bca7cba92a01","datavalue":{"value":"Formal methods","type":"string"},"datatype":"string"},"type":"statement","id":"Q1764432$B313BBF3-EB41-4D8B-8DBF-119352285643","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5dbea3b7a4fd624a725c57b582cb4fa8b701ecae","datavalue":{"value":"Hardware verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q1764432$73C11A2A-B0C1-4EF8-989D-229DC806D481","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"73d06a4412ba7c7a4b2c38ca2a6c070deb2b732a","datavalue":{"value":"Type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q1764432$C6D41E7A-A546-461C-8049-C5B221836E11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d689545ad90ec452abc573f6acd6090e6b7a7d27","datavalue":{"value":"Dependent types","type":"string"},"datatype":"string"},"type":"statement","id":"Q1764432$3AA32179-B1E1-4D24-8B91-DC8776E9ECA8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7567c46de54616eedfe44af80c618b799f5adc25","datavalue":{"value":"Co-induction","type":"string"},"datatype":"string"},"type":"statement","id":"Q1764432$1ACAF05A-E7CE-4E67-A671-DF3AE545CF42","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9806832c3a75cf19bb88043be076c30b5b4add83","datavalue":{"value":"Extraction","type":"string"},"datatype":"string"},"type":"statement","id":"Q1764432$86B1C362-EC2F-4F12-8FF8-1E0E781B99BE","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1764432$8160BFEB-9A3D-41CE-BCEC-A5E0951B2DE2","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":"Q1764432$ABA77E10-245E-4119-8152-5814517DC9BC","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"c9053afe83d71bb4eccefb38238f55d0b62e0154","datavalue":{"value":"https://doi.org/10.1007/s00165-004-0048-3","type":"string"},"datatype":"url"},"type":"statement","id":"Q1764432$F66B959A-4CDD-432B-9257-BD891E08F5A9","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"4eda1e56ad472eac25b3c8cbdb4461fc87eee767","datavalue":{"value":"W1996451615","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1764432$A7BE3DEA-9141-4CD1-8DD6-765A25A07862","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"1c5f923b9047ae1dc2ce5cb7046db98d02bef412","datavalue":{"value":"10.1007/S00165-004-0048-3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1764432$D48CE563-2F91-4A5D-9B97-45CF43F972C9","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5d70d5ce8b63a6d88c2164ea8975126b43fca81b","datavalue":{"value":{"entity-type":"item","numeric-id":3100217,"id":"Q3100217"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"23340cc8c3b031157a1e2e6b2aed48c268c2b693","datavalue":{"value":{"amount":"+0.8287219405174255","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":"Q1764432$0CED72F5-A00E-4B26-AF1C-770C0978C73C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c67ce830460fce6490695f648f245185c96a691a","datavalue":{"value":{"entity-type":"item","numeric-id":4647582,"id":"Q4647582"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"eca19ae2d61fc27f846e9a4660adab6897d28a58","datavalue":{"value":{"amount":"+0.8264175653457642","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":"Q1764432$37745A11-FB90-4EA9-9EAB-BD46A2CB4024","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"db9adde6ab07d19599d8e23df92b13a8b6e87b55","datavalue":{"value":{"entity-type":"item","numeric-id":4580232,"id":"Q4580232"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a75c4ed8ca67c4f6a29b011bfce1a2a00a1e758a","datavalue":{"value":{"amount":"+0.7510334849357605","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":"Q1764432$AF2537B1-B7D2-443E-B81F-37655AE8D261","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b42b0f154574fe6f9093d1067ca431c00e19f7e6","datavalue":{"value":{"entity-type":"item","numeric-id":1791197,"id":"Q1791197"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0cd4599275e83443dc78552f9f5b2a808f231576","datavalue":{"value":{"amount":"+0.7470667362213135","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":"Q1764432$51A45E5B-EDC8-414A-A35A-A2EACEE67A5C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"085d01fd3d5b64326f9bbba67b5309731c5b996b","datavalue":{"value":{"entity-type":"item","numeric-id":1856145,"id":"Q1856145"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f5c49dafc67bc00a22833d097aedc2c920434381","datavalue":{"value":{"amount":"+0.7348207235336304","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":"Q1764432$5DB9C025-A156-41A0-9120-19973E37BDF5","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1764432","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1764432"}}}}}