{"entities":{"Q1408657":{"pageid":1419397,"ns":120,"title":"Item:Q1408657","lastrevid":68784780,"modified":"2026-04-13T02:03:07Z","type":"item","id":"Q1408657","labels":{"en":{"language":"en","value":"Proofs and programs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1985795"}},"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":"Q1408657$354BA2D5-5AF2-48ED-8EA0-ACD202D252C3","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"a387372d4a14f9f5724cda0aefdbadf96a8539d8","datavalue":{"value":{"text":"Proofs and programs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1408657$BF763B5C-74F0-4BBF-936A-65EB073DE2E4","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"b3143e8c0de7c0d99577e89b9d37cd51076fb92a","datavalue":{"value":"1055.03033","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1408657$7FA88ECC-0FBE-4FCD-B061-6B4032ED24C4","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"7a92c578f66f113c832193c69fad5675d5ba07ed","datavalue":{"value":"10.1023/A:1022135614184","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1408657$EF4652AA-2655-4608-B996-67364B2650EA","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"28921346d64a666ce2dd47540df2f388e07634f5","datavalue":{"value":{"entity-type":"item","numeric-id":162813,"id":"Q162813"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1408657$F856CAE6-1F4E-4A30-BB6E-A1ECF19A661F","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"f37244814e4fbe2fab0838dfe21d7174c9a47265","datavalue":{"value":{"time":"+2003-09-25T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1408657$37611F93-0705-4DF5-8FA2-C505BDAE9369","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"f1d8f4be9732a3ea2cd5db05207e2e89f23852b9","datavalue":{"value":"This paper is a general presentation, very readable, of the use of \\(\\lambda\\)-calculus as a system of notations for proofs. As said in the introduction, this can help in the design of interactive proof systems for making computers do mathematics, complementary to computer algebra systems that aid algebraists or analysts in doing computations. Various relevant aspects of the theory of \\(\\lambda\\)-calculus are presented: \\(\\lambda\\)-calculus notation for proofs in natural deduction, Hindley-Milner algorithm, semantics of \\(\\lambda\\)-calculus, polymorphism and its semantics.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1408657$2D8F5D8F-2FE1-424F-A571-09FAA603BD12","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"256f7e8a78354c9241b063a26583c1bfdf31ddc2","datavalue":{"value":{"entity-type":"item","numeric-id":375196,"id":"Q375196"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1408657$246A7120-5C78-49CD-8486-7FEB00075207","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"d971f250f4b60bd91da7e9350568180af141e6af","datavalue":{"value":"03F03","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1408657$E9F0FCE2-A0FB-4278-BCD4-4FF00F258C76","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"25aa969dcca62ee94c95b2a54e4102ee8a17d130","datavalue":{"value":"03B40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1408657$DC371CAC-06E1-4B38-86FD-68D466A7D8F6","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"cbf3994fc22a852875b4dffad960759aa1b5207a","datavalue":{"value":"1985795","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1408657$BDA34361-0240-4520-AFE3-77941E2A582B","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"96125518bbd73c679654439d2a0c9178b4d2695c","datavalue":{"value":"\\(\\lambda\\)-calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q1408657$4E34EE76-B344-4C57-A809-E0D843D8D94F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f89b34d84a29901e6cfe557573b31fa1373d9525","datavalue":{"value":"Curry-Howard correspondence","type":"string"},"datatype":"string"},"type":"statement","id":"Q1408657$5F85DF5B-5E8B-4ADF-BF12-78CC3BEC25F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5ea0e35eece84bed33461e424b92d07e45bd0c24","datavalue":{"value":"type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q1408657$29AB9900-B8D3-4BEF-947B-A86792DC499C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c47bd69800ec9a3c8fdb3c483630a46ac282cb0d","datavalue":{"value":"polymorphism","type":"string"},"datatype":"string"},"type":"statement","id":"Q1408657$EF8EC5B2-998D-4999-850D-CC690A7400FF","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":"Q1408657$9D39B963-D471-4E1B-817E-030B49FB4D49","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"787bce44c26bfa68c4bdd6a337d32f1925d9a163","datavalue":{"value":{"entity-type":"item","numeric-id":3757915,"id":"Q3757915"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4594c01f206a3a3bedca581f712e6fc110ec660e","datavalue":{"value":{"amount":"+0.9686986","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1408657$40085E18-656A-472B-B790-0DABE1451AAC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c9ddfdd0c0639e442b2aadc92973a7dfa0dd16ad","datavalue":{"value":{"entity-type":"item","numeric-id":4733861,"id":"Q4733861"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4bb9d9f429f953e40936865cf181478b2fe6e865","datavalue":{"value":{"amount":"+0.96869856","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1408657$56348471-2535-4D4E-9036-8780C3FD663F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2d8068e23ea20162c700746f9d165209e24f53b1","datavalue":{"value":{"entity-type":"item","numeric-id":3219093,"id":"Q3219093"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"25b01da0289033909d09d7070f8f8f35bc4503e6","datavalue":{"value":{"amount":"+0.9665277","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1408657$88035F6F-7451-435D-8533-E7204F74CAF4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9a89dc3f8b9c614d3c47ec807c896f5b07eb80c1","datavalue":{"value":{"entity-type":"item","numeric-id":3138828,"id":"Q3138828"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"25b01da0289033909d09d7070f8f8f35bc4503e6","datavalue":{"value":{"amount":"+0.9665277","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1408657$28685D4B-5478-4013-B2EC-FD083294C690","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ab6ba7746db3411117fef3a34be889dfb4c4e69a","datavalue":{"value":{"entity-type":"item","numeric-id":5448310,"id":"Q5448310"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2e227d2559c221da82be176c1d452f9d2dd81e7c","datavalue":{"value":{"amount":"+0.9658687","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1408657$1756F066-A014-4E3D-A6DB-217207D9C60C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6b6b13962684c8466629888c66ea6edcf94e7000","datavalue":{"value":{"entity-type":"item","numeric-id":3576189,"id":"Q3576189"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a4d455b96560b655aa25089178e196cf0f1f0979","datavalue":{"value":{"amount":"+0.9538063","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1408657$B8DA8E70-C3D8-47E7-AFB4-933C75DF0516","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d43c8caecbde7694f12ec3164da9e4d96d586bac","datavalue":{"value":{"entity-type":"item","numeric-id":693063,"id":"Q693063"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a4d455b96560b655aa25089178e196cf0f1f0979","datavalue":{"value":{"amount":"+0.9538063","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1408657$D1F1AFE5-C1FA-4006-94F8-D10FF8BBBC8D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3c26251f6824bc527e5a652aa3aafa9332146550","datavalue":{"value":{"entity-type":"item","numeric-id":3032255,"id":"Q3032255"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"91ae543fc7c2c0eb3d3b8989b97fbe084dc679ea","datavalue":{"value":{"amount":"+0.9536699","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1408657$12FCD301-191C-455C-AEBD-23154DD3CF6F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"886dcdc037c492e6d0c901743a6d0c736287bcc0","datavalue":{"value":{"entity-type":"item","numeric-id":3608399,"id":"Q3608399"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7a14d661d5a9449785d7164567ec56174c2f8afd","datavalue":{"value":{"amount":"+0.93643785","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1408657$45D9A611-467A-4308-9FC9-2951263985AA","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"03c3b74ff26c086a7988af4846b84322637129ef","datavalue":{"value":{"entity-type":"item","numeric-id":1868461,"id":"Q1868461"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1408657$D3E47382-B80E-472E-A578-84994B64DBD2","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Proofs and programs","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Proofs_and_programs"}}}}}