{"entities":{"Q6970262":{"pageid":21324636,"ns":120,"title":"Item:Q6970262","lastrevid":84048233,"modified":"2026-05-08T19:29:04Z","type":"item","id":"Q6970262","labels":{"en":{"language":"en","value":"Primitive recursive dependent type theory"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 8053993"}},"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":"Q6970262$23D9A876-5E2E-4A68-97A1-B870F132DAB8","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"10891271b23dae9caff7724b644e08727b7c5545","datavalue":{"value":{"text":"Primitive recursive dependent type theory","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6970262$1D7968EB-4718-4A12-B900-462812DE4E0C","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"d11d469f6bfd11f20216fdf4b099fe71fac7a2ec","datavalue":{"value":"1573.03129","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6970262$9005F7BE-1E5D-4D38-BA0F-CE084B790E13","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"96757cd5889971ed835890c9c64218d8a05db93d","datavalue":{"value":"10.1145/3661814.3662136","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6970262$EF191425-D4F8-4FE9-940E-89341C231D4D","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"07fa863ace5e5643256336648f47ae5f74824fa1","datavalue":{"value":{"entity-type":"item","numeric-id":6970261,"id":"Q6970261"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6970262$6C2329AF-ACB7-4BD3-9B80-12556F421777","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"60c0cb0b5a75ad9f1f257059f0eca6fe552d3e54","datavalue":{"value":{"entity-type":"item","numeric-id":6970258,"id":"Q6970258"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6970262$BF8B33C7-FE9B-45D4-98EE-F9B16BDA7ABF","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"66c9695eb20dc9e6bcc46cab6b3e0d2faaff014c","datavalue":{"value":{"time":"+2025-06-18T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6970262$42DDFE57-1938-4AD6-BA4B-1C9720E2E9E7","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"d9230c8da6e5632ad621620269b7ca185454f9df","datavalue":{"value":"03B38","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6970262$E11D9E12-B5F3-437F-9C21-5210ED3F5B31","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"5644d401414ce5ae4b001cc35a247cae358bc939","datavalue":{"value":"8053993","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6970262$69D362E3-0D76-4A70-9FAC-BCFE5F6CAEA5","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5ea0e35eece84bed33461e424b92d07e45bd0c24","datavalue":{"value":"type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q6970262$173CB5D1-D874-40BE-BB18-51956C8CA446","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"83d5dcaa7aef3dc9ddc3eab92a7db35d53442c07","datavalue":{"value":"proof theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q6970262$AB8BD7C8-41DB-454F-A36B-1B473EF16E16","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"34ae3a8d9f3401a083509ec6ab2b6f0f2deb2a29","datavalue":{"value":"formal metatheory","type":"string"},"datatype":"string"},"type":"statement","id":"Q6970262$AA52E5E1-A90D-4525-A55E-A7554CD04487","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8ef1059ded76113e8a55895e9c6444f3ab0f16cb","datavalue":{"value":"primitive recursive arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q6970262$DE105E24-5705-49BE-B59E-9C0CA6393112","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":"Q6970262$A46BD85D-24E8-4E4D-B0EB-8C8527044BA7","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"b7ae45f11d039b13e3537bd38c8b726270d8fca6","datavalue":{"value":{"entity-type":"item","numeric-id":1437034,"id":"Q1437034"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6970262$73419717-4F02-4095-8CB6-E259AEA0A976","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8324ecf1b83629f49a2cf02432ea440e2d5e9d22","datavalue":{"value":{"entity-type":"item","numeric-id":5145276,"id":"Q5145276"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6970262$286951DD-90BA-46D6-B47B-BC60984E02F9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"468e91b711762444f3218471e1feccac4a79e420","datavalue":{"value":{"entity-type":"item","numeric-id":2968413,"id":"Q2968413"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6970262$452C05CB-0003-4C0C-B4EA-3B7CCD2A653E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c16f13bffab4a9a13fe0266618d7e8ba5ed4b8de","datavalue":{"value":{"entity-type":"item","numeric-id":6622055,"id":"Q6622055"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6970262$3BBAA66E-23FF-422A-A2F5-BDABF89ED786","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fd3c1ad58f8d3ff5f9672b1fd7f4ce922b034d87","datavalue":{"value":{"entity-type":"item","numeric-id":4435459,"id":"Q4435459"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6970262$816E8CC2-5F66-4CA8-8929-48682A960E60","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b0750119319825b48163ea7e9aaeedc16167046c","datavalue":{"value":{"entity-type":"item","numeric-id":3612623,"id":"Q3612623"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6970262$CF81B0B7-C155-4671-AA31-21550799150D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4b7fccd560221ea7f03064eaf67187aa99c6ef8f","datavalue":{"value":{"entity-type":"item","numeric-id":5697711,"id":"Q5697711"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6970262$F2055DBA-2AE1-4A8C-BAFC-30A1E0EF8460","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6224b375b18b97f01436004cb27e211f581673b6","datavalue":{"value":{"entity-type":"item","numeric-id":4790656,"id":"Q4790656"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6970262$A214B70D-D3C8-4C04-9A7B-5EB00960E515","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d65a1c5241cd7b9ba7b996dda44d950b8f5a9faf","datavalue":{"value":{"entity-type":"item","numeric-id":5704004,"id":"Q5704004"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6970262$2B9F1CC8-BFBA-47A4-91ED-952651634E76","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"21bcc30b765cca771213ef9a1977f71c8871dbe4","datavalue":{"value":{"entity-type":"item","numeric-id":5310638,"id":"Q5310638"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6970262$2C8572C1-E821-4EAD-8DDB-DAA5373C3A83","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a4fd098ea4c8653eaec826e6d53d5157343c914f","datavalue":{"value":{"entity-type":"item","numeric-id":4580226,"id":"Q4580226"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6970262$63BBE0DE-B863-4C63-A2D2-C8E1057AAAAB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"05618bc94dd537d3034b233a45ab1cb0906c9164","datavalue":{"value":{"entity-type":"item","numeric-id":3196622,"id":"Q3196622"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6970262$4E860E7A-9F54-4B6C-8F17-595FC20C0E6E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e622fcb1779edff63dfc667212e670505009e914","datavalue":{"value":{"entity-type":"item","numeric-id":5155672,"id":"Q5155672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6970262$B3043843-0248-4AFA-80BF-9B82FA0EF20B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"44cbf1fc2616a90273e8d3db1d96fae28ad400e1","datavalue":{"value":{"entity-type":"item","numeric-id":4218937,"id":"Q4218937"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6970262$3C0B4F8D-BBFC-47B0-BEA1-968409D87CB0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"387ee51290294bfca1aa47ce45ebff34bfe7f231","datavalue":{"value":{"entity-type":"item","numeric-id":4382502,"id":"Q4382502"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6970262$FB5726CE-D10D-4A92-90EA-B14A67085B49","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2fffc5404ef5f22452974abc741a98522b92bfdd","datavalue":{"value":{"entity-type":"item","numeric-id":1577481,"id":"Q1577481"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6970262$1F2627AE-98D5-4E33-837B-28E820E6E360","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"35abd1a50713a72ac28ac0b5461d848f396ff09c","datavalue":{"value":{"entity-type":"item","numeric-id":5014598,"id":"Q5014598"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6970262$9E10A580-394F-4AFC-A7E0-B450EF031C76","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cc8d8017a61ff15ede0a457fc81ea2efc67f684a","datavalue":{"value":{"entity-type":"item","numeric-id":4182745,"id":"Q4182745"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6970262$5186571F-F4AB-40EA-8256-DF492A797630","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e3c6d07dd80de4de8f6f1d51aa5d78e790a6fd51","datavalue":{"value":{"entity-type":"item","numeric-id":5812175,"id":"Q5812175"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6970262$A5E6ADDD-E32E-4C07-8BC1-690329B8E444","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b609c310cf6b1ace68a1cde0b501aa8f33cf6066","datavalue":{"value":{"entity-type":"item","numeric-id":2700785,"id":"Q2700785"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6970262$3925F35E-E163-4D49-99D5-F6CB3AEAEC09","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d82b227295c10b6c3c9289b01dc8016d6c611441","datavalue":{"value":{"entity-type":"item","numeric-id":3727946,"id":"Q3727946"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6970262$7973DB2A-3416-4CD7-ACD6-20EC1E5A0063","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ba7acd0e33cf62ff42c5d3d2963429fca167fec9","datavalue":{"value":{"entity-type":"item","numeric-id":5111322,"id":"Q5111322"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6970262$5E37C16D-D152-4E55-9762-43D03A2AEB82","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fb83562c2d416412c17636480881d95b7979cd02","datavalue":{"value":{"entity-type":"item","numeric-id":3552042,"id":"Q3552042"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6970262$A1386A8F-613C-48E8-B375-906FF641ADB1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d223355713d43fd22fdbfdb541ce3efab0d3390a","datavalue":{"value":{"entity-type":"item","numeric-id":1238016,"id":"Q1238016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6970262$B484ADE6-5D01-4CE0-AC02-D0CE344BE373","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":"Q6970262$C604F0CB-48BD-46E4-8BA4-3C517C9E35CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8fedad9fb77d32b62f8a221ccdcce910bcfa5967","datavalue":{"value":{"entity-type":"item","numeric-id":1822604,"id":"Q1822604"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6970262$C219B279-3994-421B-B4F0-A45E474DCE09","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0430e4a9fe16a78c945c278746cad2959afea463","datavalue":{"value":{"entity-type":"item","numeric-id":3395521,"id":"Q3395521"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6970262$6FEE1492-D0ED-4DFF-84A2-C61F388F82EF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"890522dc4e3ecb3007fccfde8c53acf4163b6c1a","datavalue":{"value":{"entity-type":"item","numeric-id":5420262,"id":"Q5420262"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6970262$FF4E7B01-1E97-416F-B8AB-6EAE59DCA597","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Primitive recursive dependent type theory","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Primitive_recursive_dependent_type_theory"}}}}}