{"entities":{"Q1201296":{"pageid":1212045,"ns":120,"title":"Item:Q1201296","lastrevid":66861981,"modified":"2026-04-12T13:21:42Z","type":"item","id":"Q1201296","labels":{"en":{"language":"en","value":"Coquand's calculus of constructions: A mathematical foundation for a proof development system"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 97536"}},"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":"Q1201296$C7F7F04F-D09B-4E66-B399-A1F268DB3A92","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"cddbabffb894d5f7db043154709368f6e92b5cbb","datavalue":{"value":{"text":"Coquand's calculus of constructions: A mathematical foundation for a proof development system","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1201296$3EE3568C-3637-4B62-9574-27E1A616DB21","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"1601814c3c7bd9dc28586bf3d0fbc99c4c745ded","datavalue":{"value":"0766.03007","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1201296$3012B218-D17F-42D6-86B6-7B5A683AF087","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"605c3ef602f38d56ddc8022efec9c4cd579c5e3e","datavalue":{"value":"10.1007/BF01211392","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1201296$D208B32B-F2F4-4B54-B17E-83F9EED9F5AD","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"d1c8a82181abf50fa906f6fa96d701d7aa12bbdc","datavalue":{"value":{"entity-type":"item","numeric-id":242949,"id":"Q242949"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1201296$29737EB4-7F49-4B02-969A-87189DD158AA","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":"Q1201296$563E75A4-FD5F-4923-AE66-0291323921D3","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b0879f591850b4f9f14b2c481d3e08995aa22089","datavalue":{"value":{"time":"+1993-01-17T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1201296$4E5A2660-98BD-41F0-9D14-3626FDD70CFE","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"25aa969dcca62ee94c95b2a54e4102ee8a17d130","datavalue":{"value":"03B40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1201296$33C768F8-6B56-4B50-823D-DF59307E5976","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d971f250f4b60bd91da7e9350568180af141e6af","datavalue":{"value":"03F03","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1201296$EDEDED18-A1BA-4E78-94CE-B5A77C46F624","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1201296$108ECB5A-CB24-4FEE-8C43-A144D5E9DBF9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"f3a45d3b9170142354a54e44062b715a09cdd0db","datavalue":{"value":"68N15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1201296$AA161D73-397F-489C-BACD-8C360C7AC0F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"02303c61036060136df3f7b7e22c52163746633f","datavalue":{"value":"68Q99","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1201296$B097B963-B335-4881-8206-5A11653D5853","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"a64982bb2357baacdbdb7cb2f0901a011330cd0a","datavalue":{"value":"97536","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1201296$6DD8D920-A100-46CA-9C58-B2FEA2186625","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ca15f19c0d5371a14b57a8971bc71186b06148bc","datavalue":{"value":"consistency of assumptions","type":"string"},"datatype":"string"},"type":"statement","id":"Q1201296$2FD9DB47-D0EE-42EB-8C69-DE936E60D8EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"aacdd9e6b1e081b5de4688ca768accb91a2c66bc","datavalue":{"value":"calculus of constructions","type":"string"},"datatype":"string"},"type":"statement","id":"Q1201296$0D0864B7-CA4A-43DF-9E84-A69EF78E0C12","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1e7d764d513feb5ba68ce61a9a148c09d73fdaf0","datavalue":{"value":"higher order typed \\(\\lambda\\)-calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q1201296$DD593CA7-EEB5-4778-A59E-F963D61E1EF9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c8ce9405f3184f895eba448b437163b21c987320","datavalue":{"value":"proof development system","type":"string"},"datatype":"string"},"type":"statement","id":"Q1201296$E5990D69-E9AA-4879-8F91-8B8EEF869DF5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"00134f94fae617052450fe78ce4e8e7c792fddd5","datavalue":{"value":"normalisation","type":"string"},"datatype":"string"},"type":"statement","id":"Q1201296$57959B8B-2446-4AF9-9A9E-42D4D4A1E197","rank":"normal"}],"P1463":[{"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":"Q1201296$A84F70CA-1C4F-4EBB-9893-69F774A823AF","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":"Q1201296$C928F268-8FFB-4123-895A-A09D25C7A266","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"5cb9e3a6772849ff9a629cad139288838375d09c","datavalue":{"value":{"entity-type":"item","numeric-id":2395467,"id":"Q2395467"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1201296$19639DFC-02AE-4DEA-A9AD-AFB54F06E348","rank":"normal"},{"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":"Q1201296$16F1E1F6-75AA-43EC-8426-CC91CDEDEE60","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"15ffb46be9e49b237f6fde18c89e459513c877e1","datavalue":{"value":{"entity-type":"item","numeric-id":5547552,"id":"Q5547552"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1201296$6BB8AA0A-B660-4553-BD9D-8ECCC03FE5A5","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":"Q1201296$D55973EA-E9F7-4A23-B9AA-339321EDE5DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"77f473aa08523f9a9a313b9aaded66a723dd75c9","datavalue":{"value":{"entity-type":"item","numeric-id":2553958,"id":"Q2553958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1201296$F612453D-68B1-4EC0-B581-0B21913459B0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84ad42be65af5dfa9e512f666229d02ed5041b60","datavalue":{"value":{"entity-type":"item","numeric-id":3856127,"id":"Q3856127"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1201296$99403095-157D-4932-AD9E-F221D6D6031D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"70d5dcacdf82491509f047ffa7adf630e71ade90","datavalue":{"value":{"entity-type":"item","numeric-id":5667469,"id":"Q5667469"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1201296$87B727AA-B6DB-467A-A021-01FB0A3B16B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f660261386a269c5c6d007e1774c790f4ddf72ec","datavalue":{"value":{"entity-type":"item","numeric-id":5815602,"id":"Q5815602"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1201296$0FCA0211-62DA-4129-B40F-4CDD0A432F71","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f23417d0146cdc8808662ea4f0b0496e878f3547","datavalue":{"value":{"entity-type":"item","numeric-id":4722037,"id":"Q4722037"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1201296$C9875567-DCA5-4F21-8D04-73E599AE02ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e04882dd0098e511c274267f86b00f5c3a4c9815","datavalue":{"value":{"entity-type":"item","numeric-id":3211296,"id":"Q3211296"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1201296$8FCA63D0-D8F0-4144-8C2C-66C66EF3EE92","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":"Q1201296$F870A640-8B21-484B-AC36-97E4E3819125","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b8d95625ec9e5b7c46cee42d87256157d982706a","datavalue":{"value":{"entity-type":"item","numeric-id":5559220,"id":"Q5559220"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1201296$7BA25E2F-2FA8-43DA-9981-7A9C43959546","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d45f47c65cbf54bc3759bb5ab2a9b9b91e856ab9","datavalue":{"value":{"entity-type":"item","numeric-id":4147961,"id":"Q4147961"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1201296$AEFFA6F6-15F2-4AFD-8E36-E035CD4CAA32","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5a821ac499f0496c149a9b10288f471c76016ba7","datavalue":{"value":{"entity-type":"item","numeric-id":5961667,"id":"Q5961667"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1201296$193F60EB-C296-4A40-A0A3-4B0DBDB307E2","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"f69fb25c170ea608253fe217d03445f16508d5ee","datavalue":{"value":"https://doi.org/10.1007/bf01211392","type":"string"},"datatype":"url"},"type":"statement","id":"Q1201296$BB87A279-143D-4E92-9556-939BAAD9F7EB","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"938a55a7cabaccdf757e3ef0a136e9c7e0c0902d","datavalue":{"value":"W2012195956","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1201296$D995B2D7-00B3-418E-9421-E0BDF895C14E","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"229fa832c9f679ac8d467437b0c437e298bca5df","datavalue":{"value":{"entity-type":"item","numeric-id":5961667,"id":"Q5961667"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4476477526223fb29a5849a301f6747b55822f71","datavalue":{"value":{"amount":"+0.8372969627380371","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":"Q1201296$E1FC10AF-A7A1-4FB6-853F-3878EEF61AE2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b04fc28ff935556a5c4174aab3a7627efd13f38b","datavalue":{"value":{"entity-type":"item","numeric-id":1108266,"id":"Q1108266"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5fd9d1f5d46db41e41036626ca29405c870fa4b5","datavalue":{"value":{"amount":"+0.8334287405014038","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":"Q1201296$8CB98892-5812-4B02-B1FC-20C41A38BE6F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fef6ecccd9c3863140c9acc43b3d048362b40b79","datavalue":{"value":{"entity-type":"item","numeric-id":3030827,"id":"Q3030827"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"31751604cd82230b469c2da1f047a7113b900785","datavalue":{"value":{"amount":"+0.8299687504768372","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":"Q1201296$DE70B17A-6392-41AA-8BF2-663A22DC3D53","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"387cce94216297b66f69d2aa4feef49d02d8cfd3","datavalue":{"value":{"entity-type":"item","numeric-id":4681362,"id":"Q4681362"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bf5e0ad8ccb9c6b172a6ec7c5e658ff7657f502d","datavalue":{"value":{"amount":"+0.7981102466583252","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":"Q1201296$6511C4C2-2082-4AD5-B735-AC8F66A811E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a299ada1677cb50f9badc2dfb747cce9998463ae","datavalue":{"value":{"entity-type":"item","numeric-id":3026376,"id":"Q3026376"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"94f2e6efbb56d877359906520d56f6112d61b2d9","datavalue":{"value":{"amount":"+0.7876847982406616","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":"Q1201296$77B839E1-9D15-467E-AF59-67B062A78158","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Coquand's calculus of constructions: A mathematical foundation for a proof development system","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Coquand%27s_calculus_of_constructions:_A_mathematical_foundation_for_a_proof_development_system"}}}}}