{"entities":{"Q1097045":{"pageid":1107797,"ns":120,"title":"Item:Q1097045","lastrevid":66682170,"modified":"2026-04-12T11:53:56Z","type":"item","id":"Q1097045","labels":{"en":{"language":"en","value":"Derivation of a parsing algorithm in Martin-L\u00f6f's theory of types"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4033122"}},"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":"Q1097045$D2F993DF-9E1A-451C-AF7D-C09627824333","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"28e1f15c944b20d43ed0cb4c49509ba2364f6f1a","datavalue":{"value":{"text":"Derivation of a parsing algorithm in Martin-L\u00f6f's theory of types","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1097045$E0CFE13F-CC1C-4DC0-AEDB-DC48B1025C44","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"508eb760a960b77e9119f4b7080e2ef6b56fe25d","datavalue":{"value":"0634.68083","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1097045$FF865BC3-4704-4536-B1E5-BF2048C525A5","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"70b2a7f4d0ff79677b24a34a4c5526349a81704b","datavalue":{"value":"10.1016/0167-6423(87)90002-5","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1097045$7D7415EC-AF15-49B5-905D-FCF1C5BB076F","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e3b75a80601fa40e05e4021fa67aaf99e7bb25e5","datavalue":{"value":{"entity-type":"item","numeric-id":911742,"id":"Q911742"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1097045$42DF40E1-22EE-4E08-B784-46AE3E8340BF","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"4082512e7d3530b9726df691c7c28e9fec542a8c","datavalue":{"value":{"entity-type":"item","numeric-id":169675,"id":"Q169675"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1097045$E4AF4AF8-05E4-4128-8065-D9A67698DF32","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5ae48c61eed19d1e1e1f33f9255d5b329362d064","datavalue":{"value":{"time":"+1987-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":"Q1097045$CD297D8A-4F00-42CB-AFAF-6CD60F7B2D24","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"33f48fd86084f12d31bd08d97d09e6e2f1eadbd9","datavalue":{"value":"Type theory is a mathematical language with computation rules developed by Per Martin-L\u00f6f. Type theory was initially developed as a formalization of constructive mathematics but Martin-L\u00f6f has pointed out that it can also be viewed as a formal system for the development of provably correct programs. Here, a parser for a simple expression language is specified and a program derived from the proof of correctness of its specification using the formalism of type theory. The proof is compared with a proof of the same problem formalized in the Edinburgh LCF system.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1097045$D2AA6099-F788-4376-93FA-6C3855EEE56C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"f3affb2aa66be15f2a63c60d2aaa92bd143e6d46","datavalue":{"value":"68N20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1097045$214D5A37-6637-4B2E-9B11-BB31CF8813F9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"4cb4544bfd0397cd4a315ee326499c372f013de5","datavalue":{"value":"03F35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1097045$38691996-C1A7-4B89-B3BA-AC00ACDA8380","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1097045$99780671-4B06-4A75-87B4-0BC5BFAC877F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"092d9a7dfbbaaa84ba458f8d83190fce94c9aa54","datavalue":{"value":"68Q65","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1097045$B9087E1D-0A63-4134-823E-43F9AB17CBE0","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"eb365fc37b3600b0b373978752ace4d13a04bcd6","datavalue":{"value":"4033122","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1097045$580785B1-552E-48DA-B876-CB7D90192DC0","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"402da81208f438eccbc04d8923e81281d8add5e2","datavalue":{"value":"correctness proof of specification","type":"string"},"datatype":"string"},"type":"statement","id":"Q1097045$8E988483-EEA7-471D-A9A5-9A329A9A4FF1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"87bdda2ccc9c2599ce54291c88cc28baff4ad9f0","datavalue":{"value":"parser","type":"string"},"datatype":"string"},"type":"statement","id":"Q1097045$1B8ABAB6-F0BE-4F4B-93D2-14B2BF7B022D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c87336a9d2ad05057f92319a3caf9771d2401509","datavalue":{"value":"simple expression language","type":"string"},"datatype":"string"},"type":"statement","id":"Q1097045$2AB1F9D5-A954-4135-BC54-8AC67DA5D581","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5ea0e35eece84bed33461e424b92d07e45bd0c24","datavalue":{"value":"type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q1097045$29C8A74C-7961-4CE1-AE54-A7259811DDFB","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"25db55153babd7076d594d911b639e78d62b451a","datavalue":{"value":{"entity-type":"item","numeric-id":20369,"id":"Q20369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1097045$81123DE1-601C-4021-8829-C1184586E38B","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":"Q1097045$DD5F3582-44BD-4581-976E-548E318A1F7D","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"4f7027df5651f4db2a1c9ddce881e2197474a402","datavalue":{"value":"https://doi.org/10.1016/0167-6423(87)90002-5","type":"string"},"datatype":"url"},"type":"statement","id":"Q1097045$F494D1FE-C6E8-4EBF-AFC9-D1A7CB7E61A4","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"fbc11e37fd200fd1d131d9da5d1413b4545a77dc","datavalue":{"value":"W2031355212","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1097045$8DA7E2C2-378D-431B-AEFC-0BC4D87C38E7","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":"ef2685a5dfae6743c6ccc21c5042cac55b56ad35","datavalue":{"value":{"amount":"+0.8024747371673584","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":"Q1097045$AC52DCEF-F67A-4B30-A90A-E593EE533ADB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b215bf34512acd6bcf522fcb8600bc4a72a5aa95","datavalue":{"value":{"entity-type":"item","numeric-id":4289277,"id":"Q4289277"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c9a57521271deff353e0a4fdc7b349c0627775cf","datavalue":{"value":{"amount":"+0.7930493950843811","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":"Q1097045$2F04D648-BD23-4611-BE0E-D9061DB312E6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"30ae62e6dcd3306000dd1aa55b55e08a9450fbcb","datavalue":{"value":{"entity-type":"item","numeric-id":4028373,"id":"Q4028373"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"45fe7c1662dd23bb036d82b577a161edb2ccf39b","datavalue":{"value":{"amount":"+0.7825108170509338","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":"Q1097045$701BFCD9-73A6-4950-A037-6A452581C4D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"39027ed63c2a2a68a2e6225028f9c1d4f4901f0f","datavalue":{"value":{"entity-type":"item","numeric-id":1099173,"id":"Q1099173"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"45fe7c1662dd23bb036d82b577a161edb2ccf39b","datavalue":{"value":{"amount":"+0.7825108170509338","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":"Q1097045$3D4241A3-FC76-4CBE-ACF6-041CA4F4E5F3","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":"9b0cbfd54313d1bcdb7988055ea77ec56fad2a18","datavalue":{"value":{"amount":"+0.7647061347961426","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":"Q1097045$17C742F7-894F-48E1-87F9-D0468E81B1E4","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Derivation of a parsing algorithm in Martin-L\u00f6f's theory of types","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Derivation_of_a_parsing_algorithm_in_Martin-L%C3%B6f%27s_theory_of_types"}}}}}