{"entities":{"Q1190474":{"pageid":1201223,"ns":120,"title":"Item:Q1190474","lastrevid":66517731,"modified":"2026-04-12T10:36:57Z","type":"item","id":"Q1190474","labels":{"en":{"language":"en","value":"Program development in constructive type theory"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 55533"}},"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":"Q1190474$5CEFEE8F-FFA2-4CFF-966A-84C98936AF1F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"389ffbe8d2f865f98583027f179c565b0daebc51","datavalue":{"value":{"text":"Program development in constructive type theory","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1190474$DC281599-6C03-405E-A120-2A4579CF376C","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"2439d2519b608356ed832b6ce426cbbe1607a24d","datavalue":{"value":"0760.68012","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1190474$66F9E944-C569-4A79-B53C-336731C6CA2A","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"92f6bbac19cdf4e305c38c5a2bc1d4b827f91588","datavalue":{"value":"10.1016/0304-3975(92)90037-G","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1190474$D796963E-C283-4A83-98F5-20F3B9BFEAB5","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"c43c9dea2040a308ad1527d71ba75aae30019412","datavalue":{"value":{"entity-type":"item","numeric-id":290916,"id":"Q290916"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1190474$FD97E29D-8100-4F12-B300-C387CB25B115","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f3c424cd94a60f9664f9fb69cc6027e75cc7ff3f","datavalue":{"value":{"entity-type":"item","numeric-id":123643,"id":"Q123643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1190474$2182C319-DAC9-449A-8C2C-4B48EAE87A7F","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"d9b40ce89936be2de8343a01d1ced7ff59f76b3e","datavalue":{"value":{"time":"+1992-09-26T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1190474$AD347C9C-C2BB-4094-B747-7D7076EEE68B","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"b8e3f40e3cc87753c4e0b7d7ce4bdc00805f626f","datavalue":{"value":"68N01","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1190474$128B7ECC-87D2-4726-8589-8A29CAC95825","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"dd8503cb84d44ac2adb520ebbb11872e6dc1ec3b","datavalue":{"value":"03B15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1190474$D2760DC0-3FC3-4DB8-AAFE-BAC699AFA4D4","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"526517725ee55ff0a569193f67487d7f3e275af7","datavalue":{"value":"55533","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1190474$4D983EB9-A19B-418B-85E8-4F687A4B5CB2","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09f8ae4ad4d4e67b32938638d87b6096074ba3b7","datavalue":{"value":"program derivation from proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q1190474$26A7DCA9-6B45-4A3B-8A6C-B8E44B304521","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fe2af07b9c34ae931dc9e9986f8e4653ba857344","datavalue":{"value":"programming with proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q1190474$FBAFD9F8-0E40-4631-A03F-6B41D46372C1","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a9301974fbdbf3896f705a4c8ed840f169a9b63f","datavalue":{"value":{"entity-type":"item","numeric-id":19182,"id":"Q19182"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1190474$971A73BB-B04F-4600-AA72-177B1B79CCE3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"27b6ae20da44d6f09b655d9481cc0df08a8ffcdf","datavalue":{"value":{"entity-type":"item","numeric-id":18826,"id":"Q18826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1190474$456DD3BC-D516-48FE-9990-2B3FE575535E","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":"Q1190474$1E97ED79-BAD9-4568-8E2C-80759316413B","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"2d592f87e8857ff4d106dd1dd178161f50c9229b","datavalue":{"value":{"entity-type":"item","numeric-id":1108266,"id":"Q1108266"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1190474$312E10F1-9309-4AB5-8BCD-F52D6076F08B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"05a8530cc8341477c91a6a458d8bc3eaffcd6c6d","datavalue":{"value":{"entity-type":"item","numeric-id":1251072,"id":"Q1251072"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1190474$5A0E7B9B-099F-4535-AB58-DD9DAC64994A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4e74acf0055d8c66a56df4574c5bbeebe37656c4","datavalue":{"value":{"entity-type":"item","numeric-id":3685173,"id":"Q3685173"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1190474$B2865BF0-5AE6-4926-8BE7-462481AEC47B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"22ee85ee408ceb2acfb30c438cac3496a36c4200","datavalue":{"value":{"entity-type":"item","numeric-id":1091379,"id":"Q1091379"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1190474$334BBA95-BB17-433D-AEDB-5CD5A675AE81","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"310129a1dfe494685c71a15130e1f0861168d16d","datavalue":{"value":{"entity-type":"item","numeric-id":3478405,"id":"Q3478405"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1190474$C6DE4018-D4E0-479E-87A6-4C65CD0C0BBF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"36b355c034a15b6951cab8a2fb9dd01fb3be3dbf","datavalue":{"value":{"entity-type":"item","numeric-id":3477935,"id":"Q3477935"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1190474$9BA39AF9-64EF-4DF2-AD7B-9E49AFD5B38F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"86f69e4e3c6e6db6273645f322c23116e1ad1c80","datavalue":{"value":{"entity-type":"item","numeric-id":3343983,"id":"Q3343983"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1190474$4D17E22C-CD08-4D3A-9013-5C92146A84F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1420eb5b183c580e3eaa2025b4097787d860ff45","datavalue":{"value":{"entity-type":"item","numeric-id":1112584,"id":"Q1112584"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1190474$FD75F7A9-B19A-4350-8FD0-742A181B8E6E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d8f88db4db4ff3067bd759c8807bea327b3eccfd","datavalue":{"value":{"entity-type":"item","numeric-id":1094421,"id":"Q1094421"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1190474$0EED2B6F-81A6-4B00-8E73-9305D156C622","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1404903fbb3450c69ae4b46e148487834232fe43","datavalue":{"value":{"entity-type":"item","numeric-id":1823013,"id":"Q1823013"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1190474$3E1BE41F-B8FF-45CA-9FDA-A9EBEF437942","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"db243e20cf694a8491ba7b48de16806e33c4d296","datavalue":{"value":{"entity-type":"item","numeric-id":5096257,"id":"Q5096257"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1190474$4DD6B24F-30F1-4346-B90E-5C8867D5656F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"16f548705be118c33292ce6afa24ffd77e96b479","datavalue":{"value":{"entity-type":"item","numeric-id":3673095,"id":"Q3673095"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1190474$F20A5318-8DF8-4B28-A74D-09EFD6C512A1","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5add08a5d004f50146f4311c1ba27d67f8ad1f8e","datavalue":{"value":{"entity-type":"item","numeric-id":3477935,"id":"Q3477935"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d9524cd4da6a28eee955c098a444d369048d7682","datavalue":{"value":{"amount":"+0.8164169192314148","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":"Q1190474$2E0C6397-8E84-4C28-B121-C6DDC3825434","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"994abafcebf920ff08b53f01fe6fca3bc5aaf07b","datavalue":{"value":{"entity-type":"item","numeric-id":4038676,"id":"Q4038676"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6f9a6d576457ca0722754980634658601f74c999","datavalue":{"value":{"amount":"+0.8066462278366089","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":"Q1190474$73BE6ADA-23F0-464B-AF00-A5F77CAEC368","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"714e15e5a2ba4fff06e9121fed38d3236869a4fd","datavalue":{"value":{"entity-type":"item","numeric-id":1267035,"id":"Q1267035"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6f9a6d576457ca0722754980634658601f74c999","datavalue":{"value":{"amount":"+0.8066462278366089","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":"Q1190474$E829DB0A-7474-474D-9541-9060B81AD156","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"26cb5cd464b164ea1acb873ebe4a85f44b92d6d2","datavalue":{"value":{"entity-type":"item","numeric-id":912589,"id":"Q912589"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f810e2115251e02a2202c5a23d1af15d3035c6ce","datavalue":{"value":{"amount":"+0.7914907932281494","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":"Q1190474$AA43E4B3-EDDD-4863-AAE2-9549D30CD04B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fdf15563105d4ad85d0501988063639e6a909039","datavalue":{"value":{"entity-type":"item","numeric-id":4028371,"id":"Q4028371"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e3ad384e5d18145ee9ea47a13e7d092a14237ba8","datavalue":{"value":{"amount":"+0.7899421453475952","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":"Q1190474$0B47B104-A736-491A-B472-059C42DCED69","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Program development in constructive type theory","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Program_development_in_constructive_type_theory"}}}}}