{"entities":{"Q40373":{"pageid":40429,"ns":120,"title":"Item:Q40373","lastrevid":105426317,"modified":"2026-10-09T10:05:08Z","type":"item","id":"Q40373","labels":{"en":{"language":"en","value":"Density Compiler"}},"descriptions":{"en":{"language":"en","value":"AFP entry Density_Compiler"}},"aliases":{},"claims":{"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"9bbce4a5cbef5968c9b01fc3459936c377ffc446","datavalue":{"value":"28659","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40373$E9750BD8-2033-4924-A1B6-02C4C2A00ABC","rank":"normal"}],"P286":[{"mainsnak":{"snaktype":"value","property":"P286","hash":"b6374f10016b3132f7b015dd92e83f0e5356aaad","datavalue":{"value":{"entity-type":"item","numeric-id":2802431,"id":"Q2802431"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40373$F1CC6F24-7222-4BFA-A09C-F8DD610884B3","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40373$FAAB4997-0F5B-48CD-B576-6D93804AF8D3","rank":"normal"}],"P29":[{"mainsnak":{"snaktype":"value","property":"P29","hash":"96f4d78aa550dd89f4594881ea2610d5e89c1010","datavalue":{"value":"https://www.isa-afp.org/entries/Density_Compiler.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40373$3B10BA6A-5EA3-4383-BE49-03FF58B1D724","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"0db99c3b17fc587dc6d0b047e5ff5ce0de1786ab","datavalue":{"value":"03","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40373$7431A146-9731-4293-9CA1-02556BACA22F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"1a467a32e3049b1299c9c2b688461b7f273ec943","datavalue":{"value":"60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40373$7733F5DC-1DB2-4554-AA40-33979A854403","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"acf10290b955a69659a681d98822944f91bbad9e","datavalue":{"value":"68","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40373$C58BF19E-0C0C-48FE-83F1-5956B51770C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"541da1e359051dfcf3c498b9f1f1f8f905fbafe3","datavalue":{"value":"90","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40373$BCAD6403-A1FD-444A-9FF2-4444F9BB51EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"1a438efc028ac8f007fcfec586995516429ecdd8","datavalue":{"value":"91","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40373$ECF26A03-3C69-4F62-AAD8-C55EEB28EF91","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5f50a93e1fa52c1f7a63c5e1d98864f256220e6f","datavalue":{"value":"18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40373$811F57DF-36CE-4CBA-891F-B7CA5F3E4826","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"9ccfc2ffdb7a60cd36d8dca0a4e6d9d45f5228f3","datavalue":{"value":"3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40373$048FE721-CD4A-4FF5-B52A-2DB6DF73BA1E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"cb68336c6ece13b86917b0c80051f1685885b843","datavalue":{"value":"60.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40373$32279136-BD15-4CCC-B887-F7DA1DCD854B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"09f5e0c6033338f59ef27e37d6877da0f26d9646","datavalue":{"value":"68.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40373$C436C31C-2134-4AE2-8930-036B4AE4F286","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"1a8aa801742e290b2e6820d89349e86d8f23555f","datavalue":{"value":"90.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40373$00263827-6F77-4E95-8FEB-F0FB95A95265","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ca6833d3c12e329e13f5f7a45eb21803ac988009","datavalue":{"value":"91.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40373$DADBDACF-7159-4C60-812D-0755F2E8B2A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"6e6992288898c4b84d0375236ed98d3bb5559a8c","datavalue":{"value":"18.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40373$AA0D7B64-9FF0-410A-AE39-A9965725CCB1","rank":"normal"}],"P1458":[{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a2a767ccd0e9bdc5b1b4a2069a6679f9340a857a","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40373$002B33A3-D855-45AD-B643-7F1B7F6EEEA0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ecda3e6d8e971c0b93d4cf3afb41990e853f830f","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40373$39356132-7093-446A-95E8-0C5CE5F489FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"bb05cb23794774f62a8e4aa4de610af231973a1d","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40373$10D2B0A4-76B8-4FBD-A842-D334F636E3C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"cc41d9364226bfa8139f8dbc43b1b77967245f13","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40373$298C581F-C272-452C-A6EC-DC730CF5C9EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"03281999c3208b8f3a62eaceadadf1ce834fe219","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40373$266CA612-983C-49A4-BC19-7406CD13AEF8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"f70e8f897325b539c702d8d7cb97dfafe554224c","datavalue":{"value":{"entity-type":"item","numeric-id":32823,"id":"Q32823"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40373$5DF38526-C4A5-49C7-9368-7D97EA8F4BBD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"9ad8338290e864661fc95f2a66261cf7e07a407c","datavalue":{"value":{"entity-type":"item","numeric-id":32822,"id":"Q32822"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40373$D02154FD-0661-4EEE-A402-BCF4610B8345","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"6bbc316d4497e097d8fb3e48fd57f7643b44826c","datavalue":{"value":{"entity-type":"item","numeric-id":40246,"id":"Q40246"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40373$AB1F0A13-4C17-4E57-A1D2-D2EE133868D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"3d0f95988886eaca495735a183ff5e2ca272aae0","datavalue":{"value":{"entity-type":"item","numeric-id":24997,"id":"Q24997"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40373$3641D940-4BDA-48EE-BC28-33BFFE4F3488","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"7434bcf5c727d2c07e931aea1694436d0b39cd53","datavalue":{"value":{"entity-type":"item","numeric-id":27041,"id":"Q27041"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40373$16639D91-5812-42B7-A237-973D22B955A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"206148fb4091bc526b4985eb7106f34e5f9739ba","datavalue":{"value":{"entity-type":"item","numeric-id":52541,"id":"Q52541"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40373$39F869FC-95A9-4EA7-8684-9C0818D27E74","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"0777df209460f6d453f13a63edbbd60cf656f2b5","datavalue":{"value":{"entity-type":"item","numeric-id":40355,"id":"Q40355"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40373$12E2FF6C-4F93-4BD8-80EC-D54DD9493A49","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"244ebbac6461f60bed6d50e50ce8194b0e233968","datavalue":{"value":{"entity-type":"item","numeric-id":40296,"id":"Q40296"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40373$B4B5C355-99B4-4715-A08D-521AD6B5DB97","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"b74075817e632ca235b8b1333580f4f12e29f9fd","datavalue":{"value":{"entity-type":"item","numeric-id":40372,"id":"Q40372"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40373$C6FBE4EE-0CC2-4EF3-9E6D-390B4F0C4D62","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"868d665ea0607bf8bd28ea3e3872eb2ea87bd3d3","datavalue":{"value":{"entity-type":"item","numeric-id":40371,"id":"Q40371"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40373$1ADDD397-476F-4298-B514-4A525177D334","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"246d8bcd4bf1600a7c6d2b07f9f11f8689d33486","datavalue":{"value":{"entity-type":"item","numeric-id":40320,"id":"Q40320"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40373$AA3748D6-2177-4531-961A-857DD6C7FAF1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"03bedb439d5ea402bd9603d3cdfe1813f9fa06ca","datavalue":{"value":{"entity-type":"item","numeric-id":40356,"id":"Q40356"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40373$12944E0C-5B9E-4ED0-968F-3C81CF055FCA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"02b329e86bd44e002b407e5543cbe998c79c263a","datavalue":{"value":{"entity-type":"item","numeric-id":13928,"id":"Q13928"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40373$B50F6D11-EBD6-4167-A47C-B765B9602A05","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ed15eb8701a335444fde1bcc3327d1067ce64751","datavalue":{"value":{"entity-type":"item","numeric-id":24376,"id":"Q24376"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40373$8D9AC605-C3BB-43D7-9FCA-457666061171","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"da71442535724374fba994798fe2e776a105b283","datavalue":{"value":{"entity-type":"item","numeric-id":40255,"id":"Q40255"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40373$C6DADAAF-4FDB-4BAB-A4BC-67BFED2579C1","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"9331bd44475edee5bb221fa3fb12963c85c594ab","datavalue":{"value":"https://isa-afp.org/entries/Density_Compiler.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40373$1216D79D-4420-45AC-B6A6-AB7CD5838B3C","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"85859c7ab42dcb8b36208f2902b7ce0d86423a6f","datavalue":{"value":"Manuel Eberl","type":"string"},"datatype":"string"},"type":"statement","id":"Q40373$41C83E7B-4EF0-4898-964C-FF62759F8605","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"01b202f25e5390ba0104cc409e25272c5fbddba4","datavalue":{"value":"Johannes H\u00f6lzl","type":"string"},"datatype":"string"},"type":"statement","id":"Q40373$F9592FFA-0338-4973-8115-494DB7CE0233","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"78083bbf5b06a4f292e9e00ee445948e4fa51db5","datavalue":{"value":"Tobias Nipkow","type":"string"},"datatype":"string"},"type":"statement","id":"Q40373$F640232F-7873-417E-B32F-8FCB3B87A8D9","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"45a5024809de2c8738b443ac69e9f28c52171a08","datavalue":{"value":"Bhat et al. [TACAS 2013] developed an inductive compiler that computes density functions for probability spaces described by programs in a probabilistic functional language. In this work, we implement such a compiler for a modified version of this language within the theorem prover Isabelle and give a formal proof of its soundness w.r.t. the semantics of the source and target language. Together with Isabelle's code generation for inductive predicates, this yields a fully verified, executable density compiler. The proof is done in two steps: First, an abstract compiler working with abstract functions modelled directly in the theorem prover's logic is defined and proved sound. Then, this compiler is refined to a concrete version that returns a target-language expression. An article with the same title and authors is published in the proceedings of ESOP 2015. A detailed presentation of this work can be found in the first author's master's thesis with the same title.","type":"string"},"datatype":"string"},"type":"statement","id":"Q40373$B261B741-21EC-448D-A72E-6E31833CFBBC","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"e2c155726080b6fedb6d70ca8b94761e6f669047","datavalue":{"value":{"time":"+2014-10-09T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q40373$DA9A45EA-384C-42FC-84FF-8849FB545A4E","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"18730d495fab45c1d9955e4cccee67b90847d54b","datavalue":{"value":{"text":"A Verified Compiler for Probability Density Functions","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q40373$17FC38D9-E739-48FE-8911-DF93BCCF9E5B","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"1cd532b264c35b618a4f734d50a4a1b2a57fc0fb","datavalue":{"value":{"entity-type":"item","numeric-id":5326349,"id":"Q5326349"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40373$982D523E-E345-46CB-A350-5113DC4758E5","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40373$D05C238C-7C36-4756-9E55-D34E3D0E1DA8","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"8efbe8612495bcc999dc22ed8b71d2801a69cc6a","datavalue":{"value":{"entity-type":"item","numeric-id":7360834,"id":"Q7360834"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40373$41C7D670-7F38-4336-9530-A28FBFED744A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Density Compiler","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Density_Compiler"}}}}}