{"entities":{"Q1815797":{"pageid":1826539,"ns":120,"title":"Item:Q1815797","lastrevid":43342765,"modified":"2025-07-24T22:36:55Z","type":"item","id":"Q1815797","labels":{"en":{"language":"en","value":"Types for proofs and programs. International workshop TYPES '95, Torino, Italy, June 5--8, 1995. Selected papers"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 947230"}},"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":"Q1815797$59766353-4EC3-4646-9BA6-CAC6F727AF45","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"1b2be892da7b919fd5bf4942b005e8ae28093f9d","datavalue":{"value":{"text":"Types for proofs and programs. International workshop TYPES '95, Torino, Italy, June 5--8, 1995. Selected papers","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1815797$49DC8840-7121-4E5F-8DAA-A5A585CEED55","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"8c2ea01b6b04df51347f0699685e07ba07d3d270","datavalue":{"value":"0852.00045","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1815797$C3F08F04-4CA7-49CD-BCC0-AABEB621756C","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"d88a311706f4aca05a8912546ed96c5b43d045b4","datavalue":{"value":"10.1007/3-540-61780-9","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1815797$A5B6D9C8-2A65-4AF0-94A1-452FCA9ABD06","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":"Q1815797$5CE74813-9B03-4F3D-8588-738C6D3727D4","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"1135ee9fb3806e71456f689ba8d2084bfd3c1edb","datavalue":{"value":{"time":"+1996-11-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":"Q1815797$33374E7F-2729-47F9-BA89-E11F4A8CD7D2","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"abdaced3767b825489463d0dd5139b5a9811922a","datavalue":{"value":"The articles of mathematical interest will be reviewed individually. The workshop TYPES '94 has been announced (see Zbl 0866.00037).  Indexed articles:  \\textit{Barthe, Gilles}, Implicit coercions in type systems, 1-15 [Zbl 1434.03081]  \\textit{Barthe, Gilles; Ruys, Mark; Barendregt, Henk}, A two-level approach towards lean proof-checking, 16-35 [Zbl 1407.68431]  \\textit{Berger, U.; Schwichtenberg, H.}, The greatest common divisor: a case study for program extraction from classical proofs, 36-46 [Zbl 1434.03024]  \\textit{Beylin, Ilya; Dybjer, Peter}, Extracting a proof of coherence for monoidal categories from a proof of normalization for monoids, 47-61 [Zbl 1407.68432]  \\textit{Cederquist, Jan; Negri, Sara}, A constructive proof of the Heine-Borel covering theorem for formal reals, 62-75 [Zbl 1434.03141]  \\textit{Coquand, Thierry; Smith, Jan M.}, An application of constructive completeness, 76-84 [Zbl 1434.03098]  \\textit{Cornes, Cristina; Terrasse, Delphine}, Automating inversion of inductive predicates in Coq, 85-104 [Zbl 1407.68433]  \\textit{Curmin, Philippe}, First order marked types, 105-119 [Zbl 1434.03027]  \\textit{Dybjer, Peter}, Internal type theory, 120-134 [Zbl 1434.03149]  \\textit{Gim\u00e9nez, Eduardo}, An application of co-inductive types in Coq: verification of the alternating bit protocol, 135-152 [Zbl 1407.68435]  \\textit{Hofmann, Martin}, Conservativity of equality reflection over intensional type theory, 153-164 [Zbl 1434.03038]  \\textit{Honsell, Furio; Miculan, Marino}, A natural deduction approach to dynamic logic, 165-182 [Zbl 1434.03084]  \\textit{Magnusson, Lena}, An algorithm for checking incomplete proof objects in type theory with localization and unification, 183-200 [Zbl 1407.68438]  \\textit{Padovani, Vincent}, Decidability of all minimal models, 201-215 [Zbl 1434.03056]  \\textit{Paulin-Mohring, Christine}, Circuits as streams in Coq: verification of a sequential multiplier, 216-230 [Zbl 1407.68439]  \\textit{Ranta, Aarne}, Context-relative syntactic categories and the formalization of mathematical text, 231-248 [Zbl 1434.03079]  \\textit{Stefanova, M.; Geuvers, H.}, A simple model construction for the calculus of constructions, 249-264 [Zbl 1434.03046]  \\textit{Tammet, Tanel; Smith, Jan M.}, Optimized encodings of fragments of type theory in first order logic, 265-287 [Zbl 1434.03033]  \\textit{von Plato, Jan}, Organization and development of a constructive axiomatization, 288-296 [Zbl 1434.03145]","type":"string"},"datatype":"string"},"type":"statement","id":"Q1815797$61293D5E-0590-4DB3-9129-60995E5E92EA","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"6f2c17db95e93f9a5a19ff6c68b3a1df8b0c021e","datavalue":{"value":"00B25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1815797$6D1284B6-4BE5-479E-A2C4-2B3F68EDFEC3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ed293b811733fa9438a72e1b6ba5680a0d2aac9e","datavalue":{"value":"68-06","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1815797$E76E6A7B-0E7B-4D3B-A0AD-14A61D1DD4A2","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"70000e912e461bb36506763cd404001013c8e0c5","datavalue":{"value":"947230","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1815797$C306F807-D7B5-4F77-A0A8-514E0252B55E","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"51b51a0dc62fe8d7fae41e8f634c032bdc06df99","datavalue":{"value":"Types","type":"string"},"datatype":"string"},"type":"statement","id":"Q1815797$85DF8CBC-DE94-44A5-8E3C-0D147B96DBAE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"365b2ad72809e114ad94e6c03e54157c8d381b4d","datavalue":{"value":"Proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q1815797$070AC356-C45F-4710-8B1C-A4D24FDC1537","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c5bd553977cc99c9ad6c7a97db0771de442861cf","datavalue":{"value":"Programs","type":"string"},"datatype":"string"},"type":"statement","id":"Q1815797$2481C7B2-98D5-4B97-8B48-4A3EE1D73A25","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f7c2172f0a2ed6197400daa3f44dae0d79725b1a","datavalue":{"value":"Workshop","type":"string"},"datatype":"string"},"type":"statement","id":"Q1815797$E853B579-3322-4F0D-9D6E-F1C2FF858EF7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5c4c4bb5a86a0fdf66f908b603f2f6975f5ef6fc","datavalue":{"value":"Proceedings","type":"string"},"datatype":"string"},"type":"statement","id":"Q1815797$2EEF2AC9-DB7A-4F3D-BF8F-50E914ED32BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"16b7b659cf8993f2c71b6a1c1a3437ea03698d7a","datavalue":{"value":"Torino (Italy)","type":"string"},"datatype":"string"},"type":"statement","id":"Q1815797$E77E54E7-BD22-41DE-B7A1-DFCEBD1B0E8A","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":"Q1815797$19F3641B-7B0B-46CE-90FB-32C5CF7D7042","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"80b28b235c2e91a76af480d0d943f4bf4e8a4792","datavalue":{"value":"https://doi.org/10.1007/3-540-61780-9","type":"string"},"datatype":"url"},"type":"statement","id":"Q1815797$3FE23F7C-4F7D-4FB6-9CC6-FB68B335E2A1","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"8cfdbf498c5940af954b5b843878c9aacfcd469d","datavalue":{"value":"W4294254159","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1815797$149D227F-2F6B-4F2B-8802-2591FA5E3CA4","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1815797","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1815797"}}}}}