{"entities":{"Q800719":{"pageid":802567,"ns":120,"title":"Item:Q800719","lastrevid":64469061,"modified":"2026-04-11T20:04:50Z","type":"item","id":"Q800719","labels":{"en":{"language":"en","value":"Propositions and specifications of programs in Martin-L\u00f6f's type theory"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 3878345"}},"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":"Q800719$35041FE9-15D5-4071-94AF-75FE913A8279","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"46ab5bce670c4e803d12cf7817b5470394a4eba8","datavalue":{"value":{"text":"Propositions and specifications of programs in Martin-L\u00f6f's type theory","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q800719$8EE730DC-7E96-45A2-8EEF-120795868B8F","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"781ebb133ee4fc750234982ea77ece69a5602200","datavalue":{"value":"0551.68027","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q800719$832DF796-C916-422F-89FE-E508E25D72E1","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"d48cef39e22094660ea03e1228a11c4c98639343","datavalue":{"value":"10.1007/BF02136027","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q800719$09ED3D46-79FE-4E37-B915-392CE16A4D7E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"eede50a5b3b0c8cecc2408751b26204b77b99d90","datavalue":{"value":{"entity-type":"item","numeric-id":800717,"id":"Q800717"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q800719$3A980748-F506-444B-B373-44847740D2C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"3b7d96d2c68882294e26baabd03e0c606a357194","datavalue":{"value":{"entity-type":"item","numeric-id":800718,"id":"Q800718"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q800719$9898C23A-7CB1-4C2B-90AA-C29D3BC01FD1","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"e560271c921b84b65a9b7f0d3fa6830623f8af8b","datavalue":{"value":{"entity-type":"item","numeric-id":188629,"id":"Q188629"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q800719$FCCE1CED-7594-4854-89EF-1DDB46F5583F","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2ee0f220147ae8bc749a64db56839865dbc4f127","datavalue":{"value":{"time":"+1984-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q800719$7A223256-5438-4A22-A307-F82150481BBA","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"777a79ab6e53d228e461b1736ce60ada1502be82","datavalue":{"value":"The constructive meaning of mathematical propositions makes it possible to identify specifications for computer programs with propositions. In Martin-L\u00f6f's type theory, propositions are interpreted as types using Heyting's explanation of intuitionistic logic. Constructing a program satisfying a specification then corresponds to constructing an element of the corresponding type. One consequence of this approach is that specifications are not in general executable. These ideas are explained and some examples of specifications are given, including a specification for a compiler.","type":"string"},"datatype":"string"},"type":"statement","id":"Q800719$5E5CB60E-285A-4BEA-AB7E-2CDB97BAED94","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"092d9a7dfbbaaa84ba458f8d83190fce94c9aa54","datavalue":{"value":"68Q65","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q800719$D81E6E89-FE3D-43E2-901E-A3A1B436DF0A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q800719$C685D95A-E6C4-458C-836D-B4D088E8C10F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"c12fc4a1e2c8baa91314a21db022a569d36ea115","datavalue":{"value":"3878345","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q800719$5F36F8A4-EB4B-4CE5-AF4D-B97A272D3592","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"df040f138da0195d6bf7ee04b2cedfdeb81adbb9","datavalue":{"value":"program specification","type":"string"},"datatype":"string"},"type":"statement","id":"Q800719$679C5AA9-A62E-4031-939F-DF0485447B02","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"33775f26030d071074f6e677c78b2fdd4159a0c9","datavalue":{"value":"Martin-L\u00f6f's type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q800719$F3644AAB-9DBA-431C-A695-1B7AB03D9853","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"901c6d511d35303a6a968c1174234f4350020c8b","datavalue":{"value":"compiler","type":"string"},"datatype":"string"},"type":"statement","id":"Q800719$3025453D-74ED-435B-ADD3-D2F5CE284D85","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":"Q800719$964ABAB5-CEFA-434C-9C27-2C0E424AB86D","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":"Q800719$0D1FA55E-1731-43DA-B5F0-C505DEDD5EA7","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"19f32365b7a322b24cf5d5cb10fef31efa05053a","datavalue":{"value":{"entity-type":"item","numeric-id":4162630,"id":"Q4162630"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q800719$125F4165-C477-4549-B84A-CE9EB22F537B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4122519b918206897f0af20a4d6bc87fe7850995","datavalue":{"value":{"entity-type":"item","numeric-id":5573965,"id":"Q5573965"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q800719$6D6C450C-5FCB-4830-9CC3-02B75FE729A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ed1f6a6893359ffbe91108962b27d4ad64b47707","datavalue":{"value":{"entity-type":"item","numeric-id":5604461,"id":"Q5604461"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q800719$2437B7F6-97A9-4145-A064-26C7F98104BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5c5ae7e408b1d1201c271e00762d47096e39a012","datavalue":{"value":{"entity-type":"item","numeric-id":4111080,"id":"Q4111080"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q800719$03F72795-3684-4626-AAF7-4B6B014A3337","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3ae542aa49195da2f0564220c3e6d6c6c5762344","datavalue":{"value":{"entity-type":"item","numeric-id":769601,"id":"Q769601"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q800719$62BE8DE5-DBBC-49A4-9BBC-F8D2B4BE1987","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2d357a47c04e8c031646a6927518ecdcc37982e0","datavalue":{"value":{"entity-type":"item","numeric-id":3262780,"id":"Q3262780"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q800719$5EA07D47-8336-4D8F-85E7-3BAABF50EA87","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f231c78aee0a9996d37683e0e5678e6c7352ac95","datavalue":{"value":{"entity-type":"item","numeric-id":5843995,"id":"Q5843995"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q800719$4BDEF758-67A9-4FE0-9EB2-1DFB61755527","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ae94f828af67e50fecbc9e4b645ed6964977b9db","datavalue":{"value":{"entity-type":"item","numeric-id":4099613,"id":"Q4099613"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q800719$76DEE520-63A3-4AA0-8348-F5535C77E121","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3ab5d7b35f67f940445411fa45c1b02bcb40d39f","datavalue":{"value":{"entity-type":"item","numeric-id":3999860,"id":"Q3999860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q800719$2249EE95-3948-4C0E-9D98-EBBC669F3193","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"481d78a79f18ce6dadeb3fc5099daa3eedefeb4d","datavalue":{"value":{"entity-type":"item","numeric-id":3959405,"id":"Q3959405"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q800719$0D6C01D4-E59E-408B-8991-4A0194C4539C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4ad4905c3ba5f825b1c47112f2dfdb7b9a3bd4a5","datavalue":{"value":{"entity-type":"item","numeric-id":793721,"id":"Q793721"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q800719$702B7F94-DFC7-4674-A92D-B0C885F094FB","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"93c3484618043a2b161eda6a99e04f1a3726a8a9","datavalue":{"value":"https://doi.org/10.1007/bf02136027","type":"string"},"datatype":"url"},"type":"statement","id":"Q800719$E32C8C02-A971-432E-BB3D-52D268DFD036","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"55542b4b399c82aa28ed10ebbff4731aed2ec1d7","datavalue":{"value":"W2057584253","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q800719$3A8A0400-35A0-40B0-8753-3B85B75715B2","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"318d6fb99941ebfef40dbeca7b4f5afc2330dae1","datavalue":{"value":{"entity-type":"item","numeric-id":3740203,"id":"Q3740203"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2a213a425daf3dece81556b89ee22dcfad694a72","datavalue":{"value":{"amount":"+0.8309013843536377","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":"Q800719$F08F2908-DD27-4529-8A1F-59F9E100C92E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c7adb91e372d96708dbca2b941b10119e0da2b63","datavalue":{"value":{"entity-type":"item","numeric-id":5951523,"id":"Q5951523"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0c030cc422c947088ab0f5976e09a2178a700833","datavalue":{"value":{"amount":"+0.8213550448417664","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":"Q800719$C49E202D-11F6-460D-BC02-5450DD2D8CC7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"978891aae9ce03b1973d803156ce9403119bfa81","datavalue":{"value":{"entity-type":"item","numeric-id":911744,"id":"Q911744"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1ec94fe92d47d6bf51b2f2b630f4d164713a6c41","datavalue":{"value":{"amount":"+0.8011509776115417","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":"Q800719$CDC86FA9-485F-4266-85BF-2EC4BFA4948B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3bacc6d2a90af26a415d0f1e5cb1ad815d32a128","datavalue":{"value":{"entity-type":"item","numeric-id":5458392,"id":"Q5458392"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d7d991b4abc1fed3b4ca46875a77e7be38fc3711","datavalue":{"value":{"amount":"+0.7977251410484314","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":"Q800719$4C6B940F-67DC-4EA0-A7CA-97A35C143616","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"320f8287a6eec1fc5a76add9faffece70bc8dbb6","datavalue":{"value":{"entity-type":"item","numeric-id":3475253,"id":"Q3475253"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6ad337b18c713e8c78dc59c988c4bdb6992e777e","datavalue":{"value":{"amount":"+0.7961981296539307","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":"Q800719$CDF36D8C-85FF-4030-8BF7-391130816A31","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Propositions and specifications of programs in Martin-L\u00f6f's type theory","badges":[]}}}}}