{"entities":{"Q704168":{"pageid":706017,"ns":120,"title":"Item:Q704168","lastrevid":63654864,"modified":"2026-04-11T14:38:22Z","type":"item","id":"Q704168","labels":{"en":{"language":"en","value":"Types for proofs and programs. International workshop, TYPES 2003, Torino, Italy, April 30 -- May 4, 2003. Revised selected papers."}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 2127080"}},"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":"Q704168$88A2ACB4-BDAA-4DBD-BCC6-8575C7F0DA57","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"a9c6665b991e762167a37d0b6ede0e485d9dbe95","datavalue":{"value":{"text":"Types for proofs and programs. International workshop, TYPES 2003, Torino, Italy, April 30 -- May 4, 2003. Revised selected papers.","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q704168$2ED04B4C-8271-4E8D-BD19-3D59152F4812","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"97b5b8320dcd625b8026683687d80de211e5cd94","datavalue":{"value":"1052.68001","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q704168$FD9F3E8B-3C9F-40ED-B2DC-38C83EE1DAD0","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":"Q704168$CC820EE9-B637-4194-915D-308A71F59C09","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"915677ea13ebe6cf8033f41f837baa84af2ec8a3","datavalue":{"value":{"time":"+2005-01-13T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q704168$75E3FA7B-FBC2-4117-B7C0-2B0B0F182F39","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"902fc6a5bbc0b3726a8cfa667a2b47bdee9a4d87","datavalue":{"value":"The articles of this volume will be reviewed individually. The preceding workshop has been reviewed (see Zbl 1019.00007).  Indexed articles:  \\textit{Adams, Robin}, A modular hierarchy of logical frameworks, 1-16 [Zbl 1100.68542]  \\textit{Alessi, F.; Barbanera, Franco; Dezani-Ciancaglini, Mariangiola}, Tailoring filter models, 17-33 [Zbl 1100.03511]  \\textit{Ballarin, Clemens}, Locales and locale expressions in Isabelle/Isar, 34-50 [Zbl 1100.68615]  \\textit{Baro, Sylvain}, Introduction to PAF!, a proof assistant for ML programs verification, 51-65 [Zbl 1100.68543]  \\textit{Berghofer, Stefan}, A constructive proof of Higman's lemma in Isabelle, 66-82 [Zbl 1100.68616]  \\textit{Bettini, Lorenzo; Bono, Viviana; Likavec, Silvia}, A core calculus of higher-order mixins and classes, 83-98 [Zbl 1100.68544]  \\textit{Bono, Viviana; Tiuryn, Jerzy; Urzyczyn, Pawe\u0142}, Type inference for nested self types, 99-114 [Zbl 1100.68545]  \\textit{Brady, Edwin; McBride, Conor; McKinna, James}, Inductive families need not store their indices, 115-129 [Zbl 1100.68546]  \\textit{Chrz\u0105szcz, Jacek}, Modules in Coq are and will be correct, 130-146 [Zbl 1100.68617]  \\textit{Cirstea, Horatiu; Liquori, Luigi; Wack, Benjamin}, Rewriting calculus with fixpoints: Untyped and first-order systems, 147-161 [Zbl 1100.03514]  \\textit{Corbineau, Pierre}, First-order reasoning in the calculus of inductive constructions, 162-177 [Zbl 1100.03509]  \\textit{Dal Lago, Ugo; Martini, Simone; Roversi, Luca}, Higher-order linear ramified recurrence, 178-193 [Zbl 1100.03512]  \\textit{Esp\u00edrito Santo, Jos\u00e9; Pinto, Lu\u00eds}, Confluence and strong normalisation of the generalised multiary \\(\\lambda\\)-calculus, 194-209 [Zbl 1100.03513]  \\textit{Gambino, Nicola; Hyland, Martin}, Wellfounded trees and dependent polynomial functors, 210-225 [Zbl 1100.03055]  \\textit{Ghilezan, Silvia; Lescanne, Pierre}, Classical proofs, typed processes, and intersection types (ectended abstract), 226-241 [Zbl 1100.03515]  \\textit{Honsell, Furio; Lenisa, Marina}, ``Wave-style'' geometry of interaction models in Rel are graph-like lambda-models, 242-258 [Zbl 1100.03056]  \\textit{Kie\u00dfling, Robert; Luo, Zhaohui}, Coercions in Hindley-Milner systems, 259-275 [Zbl 1100.68534]  \\textit{Luo, Yong; Luo, Zhaohui}, Combining incoherent coercions for \\(\\Sigma\\)-types, 276-292 [Zbl 1100.03510]  \\textit{Momigliano, Alberto; Tiu, Alwen}, Induction and co-induction in sequent calculus, 293-308 [Zbl 1100.03516]  \\textit{Niqui, Milad; Bertot, Yves}, QArith: Coq formalisation of lazy rational arithmetic, 309-323 [Zbl 1100.68619]  \\textit{Honsell, Furio; Scagnetto, Ivan}, Mobility types in Coq, 324-337 [Zbl 1100.68618]  \\textit{Soloviev, Sergej; Chemouil, David}, Some algebraic structures in lambda-calculus with inductive types, 338-354 [Zbl 1100.03517]  \\textit{Watkins, Kevin; Cervesato, Iliano; Pfenning, Frank; Walker, David}, A concurrent logical framework: The propositional fragment, 355-377 [Zbl 1100.68548]  \\textit{Wiedijk, Freek}, Formal proof sketches, 378-393 [Zbl 1100.68620]  \\textit{Xi, Hongwei}, Applied type system (extended abstract), 394-408 [Zbl 1100.03518]","type":"string"},"datatype":"string"},"type":"statement","id":"Q704168$70A5B8D3-7C88-49FC-8217-A9F7799BFDED","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"ed293b811733fa9438a72e1b6ba5680a0d2aac9e","datavalue":{"value":"68-06","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q704168$13A8321B-88FF-4C12-B33C-BDB379EAFD2A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q704168$A411ED13-6F34-4A2B-84B4-9A57A4871511","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"6f2c17db95e93f9a5a19ff6c68b3a1df8b0c021e","datavalue":{"value":"00B25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q704168$9187CAF5-DE77-4E45-A0F0-BA885FD51A5B","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"fe13cc1b6391b5a190669dfb2ab9561bce2b0d17","datavalue":{"value":"2127080","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q704168$694D59CC-87A7-430C-8B3D-06644C5A0A59","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9aeef25d5839625565921d83cf1c652bf6f2fbf6","datavalue":{"value":{"entity-type":"item","numeric-id":17052,"id":"Q17052"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q704168$201B2E58-D669-43E1-870A-4CD6A874F0AE","rank":"normal"},{"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":"Q704168$D476E9FC-6F63-4128-AF27-51BC56D18BD1","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":"Q704168$D5124874-C1F7-4B43-886D-37671C6821BE","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"1fee6d0668cbb8bb1384b720d0f9cea12732a7fa","datavalue":{"value":"https://doi.org/10.1007/b98246","type":"string"},"datatype":"url"},"type":"statement","id":"Q704168$071B077F-1F79-4284-AF84-344660B08374","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"997116d9ae8d11ec014247094e10ecd25bfd6fed","datavalue":{"value":"W4298423642","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q704168$03C0734D-6AB1-4587-A858-C67AC34A5221","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"64753b15ba5c5bacf00be58bb5ec49b804bb30d9","datavalue":{"value":"10.1007/B98246","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q704168$E0076B14-DBE8-4DC8-A626-16B494BF9853","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Types for proofs and programs. International workshop, TYPES 2003, Torino, Italy, April 30 -- May 4, 2003. Revised selected papers.","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Types_for_proofs_and_programs._International_workshop,_TYPES_2003,_Torino,_Italy,_April_30_--_May_4,_2003._Revised_selected_papers."}}}}}