{"entities":{"Q2819861":{"pageid":2830599,"ns":120,"title":"Item:Q2819861","lastrevid":42207489,"modified":"2025-05-27T21:13:49Z","type":"item","id":"Q2819861","labels":{"en":{"language":"en","value":"Fiat: deductive synthesis of abstract data types in a proof assistant"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6631339"}},"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":"Q2819861$8CA830A2-1668-4750-93B9-2D179B082284","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"d36712771166549ea28fd5cbbb67c7669efef88d","datavalue":{"value":"1346.68175","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2819861$DFE82167-F7BD-4A42-8428-CA1C02CFB7DD","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"3591d23b467733a5199dc806b687cce11aa4242e","datavalue":{"value":"10.1145/2676726.2677006","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2819861$6F0BF2A1-0219-4E4D-9566-9AF27FFD10C3","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"1d2925d733af62343b50741933d1d093dc5f330d","datavalue":{"value":{"entity-type":"item","numeric-id":2819859,"id":"Q2819859"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2819861$74AD9864-6E46-4D4A-A4D7-50ACAB4B2204","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ebd22af850026676982d2d243b86cdd14bc9a72a","datavalue":{"value":{"entity-type":"item","numeric-id":2819860,"id":"Q2819860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2819861$5FC3C92B-7128-4957-9825-EAE414394807","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ed360e5a5b6485d0ec642ab4e5a8b7cc72636740","datavalue":{"value":{"entity-type":"item","numeric-id":1791168,"id":"Q1791168"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2819861$446DA74A-98F8-4491-85C8-AE65ED8D456C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"d957a3f31f9610e79e212a1ae2ae0004027dee9c","datavalue":{"value":{"entity-type":"item","numeric-id":1702890,"id":"Q1702890"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2819861$6C02825F-09CA-4CBA-B31C-9A354749B697","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b9100613eb4830bb977ae5cf1435a6c53e940dc2","datavalue":{"value":{"entity-type":"item","numeric-id":2819782,"id":"Q2819782"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2819861$83D0101B-AFD8-4B48-9EA9-771D4E3A2A87","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"a917957632d8007b9f089349668ca3b6b937a8ba","datavalue":{"value":{"time":"+2016-09-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":"Q2819861$151CFE9A-69F3-473D-B4D5-DF7445065421","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2819861$5EAA843E-B6A8-414C-BF5F-AA1FBC4A2570","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"136db5bb8708e52501dec32644ab90fd42c4c538","datavalue":{"value":"68N18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2819861$A107D938-29D9-462E-BA35-AD8746877A90","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2819861$35506045-5A6C-4927-858C-E8744EBE83C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"092d9a7dfbbaaa84ba458f8d83190fce94c9aa54","datavalue":{"value":"68Q65","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2819861$87D44FCF-36E8-4B92-ACBE-36723C1BC4C0","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"26014646d954a460103d31e06e22cd0a5747bd09","datavalue":{"value":"6631339","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2819861$F8C14087-121F-4362-8E29-857C4FBB3C42","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7f68e29cb19b9b0e1121afce8ce26bd59bf0ce8d","datavalue":{"value":"deductive synthesis","type":"string"},"datatype":"string"},"type":"statement","id":"Q2819861$6C47FFE4-DD47-4519-AB82-BFE5A50865B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"59c4b6bc7e65359eea5e05431adf8cb7542343b9","datavalue":{"value":"mechanized derivation of abstract data types","type":"string"},"datatype":"string"},"type":"statement","id":"Q2819861$CCFAB3FE-4BD8-4C7B-A713-29A45390B582","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":"Q2819861$6825F659-9502-4051-8CDB-CD1B9FA465A9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"deccf76ad6fd5180c299730d9ce8548930a22d55","datavalue":{"value":{"entity-type":"item","numeric-id":27330,"id":"Q27330"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2819861$167CE54F-6A01-4437-B154-FA73C8910FB5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"73bf07fb0985efe0166024eb806e5cf2244671a5","datavalue":{"value":{"entity-type":"item","numeric-id":18489,"id":"Q18489"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2819861$5277BDD0-C2FF-4943-A0C9-FD9FF19F2EFA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c7abd31d6fb75aff91f2dc8613d5ee6026ea07be","datavalue":{"value":{"entity-type":"item","numeric-id":34463,"id":"Q34463"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2819861$DE9E5F54-2E8C-4E8E-B910-612D697B9F2C","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":"Q2819861$EB7BFC9B-F504-4DF0-B248-20EED2A31264","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"0b74d9eeff2b7537c971f5ec5d1b4d6969235c10","datavalue":{"value":"https://doi.org/10.1145/2676726.2677006","type":"string"},"datatype":"url"},"type":"statement","id":"Q2819861$D02DD4A9-83F2-4B1C-8822-ADACABCBAE2A","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"20c753daae558ad1d22df773bf8a83d8cce97925","datavalue":{"value":"W1976978933","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2819861$2CA6B139-F621-46EF-B013-74DF98E5C478","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"4a9aeb90b6497c0509c3f68adc0ff2ad230f1032","datavalue":{"value":"Q130983872","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2819861$6C6BDF0F-4561-47DE-A4AF-3544630D06EF","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fdc61f049f8d0b30109ea2633d86e084029eda8b","datavalue":{"value":{"entity-type":"item","numeric-id":2751370,"id":"Q2751370"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6093f873e72b60b8c399c8826b7a698e46ba028a","datavalue":{"value":{"amount":"+0.8818175","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2819861$CE47F409-D66F-462A-9833-78C1FB854F35","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"84cd93a17f57c18fd09262e4d9be653bb70f38f9","datavalue":{"value":{"entity-type":"item","numeric-id":3476793,"id":"Q3476793"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"987581328d454fe6ad7fe7c0003f9a81991df181","datavalue":{"value":{"amount":"+0.87700903","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2819861$882EEF42-67A1-4EE4-B91C-B5DD49F68308","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7cb0fbc6968e9a2f89e38fedb41ff015c9a03202","datavalue":{"value":{"entity-type":"item","numeric-id":988551,"id":"Q988551"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"87d1466b9937aebb26dbee777849dbdb67c08281","datavalue":{"value":{"amount":"+0.86975","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2819861$37D3044A-2800-4EB9-A51A-8538974AE64F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b5dcbb169f2c708b8e803982d4175da6fc4d4cab","datavalue":{"value":{"entity-type":"item","numeric-id":5464642,"id":"Q5464642"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"650620abf5aac73ad5cf0835f4322370d95ee12c","datavalue":{"value":{"amount":"+0.8660017","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2819861$A6B20CA3-C360-427C-8C60-71D272351C30","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2d57aee4dc0926b14c7cd4eb20f942c2a7b85944","datavalue":{"value":{"entity-type":"item","numeric-id":5458424,"id":"Q5458424"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3ae8fc15d98962fabf1f17fb17fbac678158a505","datavalue":{"value":{"amount":"+0.8648474","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2819861$1C108974-DB03-475E-A94B-3F178F9AAF81","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bebe5a62b96d9785a280849d04f2c10f5b1201a6","datavalue":{"value":{"entity-type":"item","numeric-id":4736999,"id":"Q4736999"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a2316aaa54fa8cadbfd411311bd2d2d7fe259077","datavalue":{"value":{"amount":"+0.8625841","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2819861$03F6FD94-17C0-40F6-9176-C128A51F2174","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"498ce556dfca5c04393f1aaf9a093578b40a7501","datavalue":{"value":{"entity-type":"item","numeric-id":4736400,"id":"Q4736400"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e74e2b0dc468ecd0e2759715a28d141684a0710e","datavalue":{"value":{"amount":"+0.8624317","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2819861$D049E479-46FD-44EA-AA97-1734A8DABD38","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"832adab52a6be03c508c7df724145ae73e85a03e","datavalue":{"value":{"entity-type":"item","numeric-id":4524768,"id":"Q4524768"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2a5b57b178c04e7a863f787ef948fe1e2010dc6b","datavalue":{"value":{"amount":"+0.86234313","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2819861$A6F6091A-DFE7-4EF8-9533-2FD67474B092","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c864e2e11aecc76e4b679c6d8bf290dd6d7245d6","datavalue":{"value":{"entity-type":"item","numeric-id":4263878,"id":"Q4263878"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6b2a35d0f40e8536f518b79be9d0509bef8da4f5","datavalue":{"value":{"amount":"+0.86185515","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2819861$5740372C-AACF-47FA-8B82-01233291433F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b97ad471e6172b61acd1f2b10b8e40a3cfe9a5bc","datavalue":{"value":{"entity-type":"item","numeric-id":3003307,"id":"Q3003307"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"909cbe68cc91114b97e631c16298da055b8672e2","datavalue":{"value":{"amount":"+0.8616863","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2819861$2F22FC9D-06AD-4750-B008-CD817CCE9046","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"76eb007b8844d6c91a78299e7c10caed3430feeb","datavalue":{"value":{"text":"Fiat: deductive synthesis of abstract data types in a proof assistant","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2819861$97D3C99B-4947-4EDC-A908-3DB103298DCB","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2819861","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2819861"}}}}}