{"entities":{"Q1601174":{"pageid":1611914,"ns":120,"title":"Item:Q1601174","lastrevid":67957452,"modified":"2026-04-12T20:28:48Z","type":"item","id":"Q1601174","labels":{"en":{"language":"en","value":"Types for proofs and programs. International workshop, TYPES 2000, Durham, GB, December 8--12, 2000. Selected papers"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1757402"}},"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":"Q1601174$A96AC036-8150-4B19-A539-879B373DF5F8","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"e364a36e104ae9989b9d533002ed4ecab4a753c9","datavalue":{"value":{"text":"Types for proofs and programs. International workshop, TYPES 2000, Durham, GB, December 8--12, 2000. Selected papers","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1601174$70D1684D-88AE-48A5-A6F0-9456B6A3D51F","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"7de85fbdad24666bd66c6c0ecbe2cc1b4ee69de5","datavalue":{"value":"0988.00060","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1601174$9909D02E-269A-49B6-9697-7D3F31364C16","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"95b3443d48b8a76517e41a4fdb701aa151762d85","datavalue":{"value":"10.1007/3-540-45842-5","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1601174$D49D8079-82C4-49F2-B39B-D80A156C2B88","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1601174$E548C24F-E2E9-417C-900E-65C3191ABBA3","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"4c27c7c0f05a747a24a0ab4d7e53da6cd04b7e8f","datavalue":{"value":{"time":"+2002-06-19T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1601174$48A83FE1-C025-4400-96F8-2055B82421A2","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"77593963c8406c9180e4b1b68d111490f5e5887c","datavalue":{"value":"The articles of this volume will be reviewed individually.  Indexed articles:  \\textit{Aczel, Peter; Gambino, Nicola}, Collection principles in dependent type theory, 1-23 [Zbl 1054.03036]  \\textit{Berghofer, Stefan; Nipkow, Tobias}, Executing higher order logic, 24-40 [Zbl 1054.68133]  \\textit{Ciaffaglione, Alberto; Di Gianantonio, Pietro}, A tour with constructive real numbers, 41-52 [Zbl 1054.03038]  \\textit{Coquand, Thierry; Takeyama, Makoto}, An implementation of Type:Type, 53-62 [Zbl 1054.68087]  \\textit{Fairtlough, Matt; Mendler, Michael}, On the logical content of computational type theory: A solution to Curry's problem, 63-78 [Zbl 1054.03027]  \\textit{Geuvers, Herman; Niqui, Milad}, Constructive reals in Coq: Axioms and categoricity, 79-95 [Zbl 1054.03039]  \\textit{Geuvers, Herman; Wiedijk, Freek; Zwanenburg, Jan}, A constructive proof of the fundamental theorem of algebra without using the rationals, 96-111 [Zbl 1054.03041]  \\textit{Goguen, Healfdene}, A Kripke-style model for the admissibility of structural rules (extended abstract), 112-124 [Zbl 1054.03508]  \\textit{Hayashi, Susumu; Nakata, Masahiro}, Towards limit computable mathematics, 125-144 [Zbl 1054.03037]  \\textit{Johannisson, Kristofer}, Formalizing the halting problem in a constructive type theory, 145-159 [Zbl 1054.03032]  \\textit{Longo, Giuseppe}, On the proofs of some formally unprovable propositions and prototype proofs in type theory, 160-180 [Zbl 1062.03056]  \\textit{Magaud, Nicolas; Bertot, Yves}, Changing data structures in type theory: A study of natural numbers, 181-196 [Zbl 1054.03500]  \\textit{McBride, Conor}, Elimination with a motive, 197-216 [Zbl 1054.03501]  \\textit{Pons, Olivier}, Generalization in type theory based proof assistants, 217-232 [Zbl 1054.03502]  \\textit{Seisenberger, Monika}, An inductive version of Nash-Williams' minimal-bad-sequence argument for Higman's lemma, 233-242 [Zbl 1054.03042]","type":"string"},"datatype":"string"},"type":"statement","id":"Q1601174$A15DE149-95DC-467E-A073-89C72D0A3091","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"6f2c17db95e93f9a5a19ff6c68b3a1df8b0c021e","datavalue":{"value":"00B25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1601174$DD409BBF-B067-488E-876A-7293A2AF277B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"f1971b12f93143b2604d15a1750f495d71fae62d","datavalue":{"value":"03-06","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1601174$B36AA7B9-57A5-4005-8AB0-A1F8A0F27BD9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ed293b811733fa9438a72e1b6ba5680a0d2aac9e","datavalue":{"value":"68-06","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1601174$022D4B33-1817-4C1F-A72E-2F1C72C1344B","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"4f7740dbda6cbfd046b2b67d499d34e752ae0ec6","datavalue":{"value":"1757402","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1601174$1F2B419D-8E5A-450A-898A-5DFDCA1A9847","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"874bd5f95e70db8883bfec8c5bc90a33ebca5f19","datavalue":{"value":"Durham (GB)","type":"string"},"datatype":"string"},"type":"statement","id":"Q1601174$0DECE32A-A5E4-42FB-B20E-BCDDB3542C32","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f7c2172f0a2ed6197400daa3f44dae0d79725b1a","datavalue":{"value":"Workshop","type":"string"},"datatype":"string"},"type":"statement","id":"Q1601174$8919E933-6373-429A-9FBC-D9826C4D8613","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"df1cfe28c346d814735dd52972c178c02b57d315","datavalue":{"value":"Papers","type":"string"},"datatype":"string"},"type":"statement","id":"Q1601174$BD9CB2BC-FBAC-4D25-B6AB-2D5FF391B2AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5d849e11179ac39f86d8f5983b7ae28ae13371e3","datavalue":{"value":"TYPES 2000","type":"string"},"datatype":"string"},"type":"statement","id":"Q1601174$3CA15634-7753-4A9E-BF39-7AFDF65667F9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"365b2ad72809e114ad94e6c03e54157c8d381b4d","datavalue":{"value":"Proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q1601174$C5CCA292-90E7-4F3D-970A-C9B653CAA5BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c5bd553977cc99c9ad6c7a97db0771de442861cf","datavalue":{"value":"Programs","type":"string"},"datatype":"string"},"type":"statement","id":"Q1601174$37B2D070-80E0-4CA3-BFAA-48E40BF2EAE7","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1601174$6CD84743-E005-4423-871A-9054233E98C7","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":"Q1601174$5BFAD2B9-81C6-4EE4-A652-8EE946DC0438","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"f5f4eee71ab14375dfd9120953a8164678257012","datavalue":{"value":"https://doi.org/10.1007/3-540-45842-5","type":"string"},"datatype":"url"},"type":"statement","id":"Q1601174$18EE3D4C-F552-40A0-9539-E9811B5B53D7","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"d4581190b1076d5b1b369b31f61834965aaa1966","datavalue":{"value":"W2796961297","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1601174$8753A70C-85CC-4CDA-87AC-86E114318090","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Types for proofs and programs. International workshop, TYPES 2000, Durham, GB, December 8--12, 2000. Selected papers","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Types_for_proofs_and_programs._International_workshop,_TYPES_2000,_Durham,_GB,_December_8--12,_2000._Selected_papers"}}}}}