{"entities":{"Q7361808":{"pageid":31520963,"ns":120,"title":"Item:Q7361808","lastrevid":105423869,"modified":"2026-10-08T13:45:47Z","type":"item","id":"Q7361808","labels":{"en":{"language":"en","value":"Jinja is not Java"}},"descriptions":{"en":{"language":"en","value":"AFP entry Jinja"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"1fa2b79678f282f433fe9298619366ea0205c2d4","datavalue":{"value":"https://isa-afp.org/entries/Jinja.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361808$3CEE3EDB-5B8C-477A-9CBF-4066707A90A8","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"46145f92c416e0014f5972c8ef4f728e7419b9b2","datavalue":{"value":"Gerwin Klein","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361808$4054880C-BBE5-48D7-B3AC-57DA6CBB5217","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"78083bbf5b06a4f292e9e00ee445948e4fa51db5","datavalue":{"value":"Tobias Nipkow","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361808$5105F67E-6EF0-49E0-A1EA-AA02676E9373","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"4a75b0d2986a5c2bf11448de6542d3ef4f7b0ae7","datavalue":{"value":"We introduce Jinja, a Java-like programming language with a formal semantics designed to exhibit core features of the Java language architecture. Jinja is a compromise between realism of the language and tractability and clarity of the formal semantics. The following aspects are formalised: a big and a small step operational semantics for Jinja and a proof of their equivalence; a type system and a definite initialisation analysis; a type safety proof of the small step semantics; a virtual machine (JVM), its operational semantics and its type system; a type safety proof for the JVM; a bytecode verifier, i.e. data flow analyser for the JVM; a correctness proof of the bytecode verifier w.r.t. the type system; a compiler and a proof that it preserves semantics and well-typedness. The emphasis of this work is not on particular language features but on providing a unified model of the source language, the virtual machine and the compiler. The whole development has been carried out in the theorem prover Isabelle/HOL.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361808$F66018A1-D3F1-4617-95BF-58AD94FC7729","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"0e4d578b35a7e3b754503335b980ec15049161ec","datavalue":{"value":{"time":"+2005-06-01T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361808$8EB6E69E-9E52-40C0-A399-950741E9D8A7","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"2e19df59c76e80f8eb1e55ca865cfcbd3fb4d291","datavalue":{"value":{"text":"Jinja is not Java","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361808$9D1EBA0C-7115-450E-9E95-EB3740E143A8","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":"Q7361808$8759B45C-925A-418D-ADB1-352A61B17307","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"e0b5465b6a0d9e05645cdb7168eee1aaf7eb2845","datavalue":{"value":{"entity-type":"item","numeric-id":7361518,"id":"Q7361518"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361808$0FD4A4EC-2A9D-4BD7-8B64-B710CC64823E","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"9beb5f7be6b27e22c4af581585b828086bbf7950","datavalue":{"value":{"entity-type":"item","numeric-id":7360796,"id":"Q7360796"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361808$0F91A770-DDB7-4CF3-8C93-638013E08F91","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":"Q7361808$BE7CA735-9304-4561-BC0E-C94C6B82BE70","rank":"normal"}],"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"990a11cc82ee251620de1c2b0d65204e992db1c5","datavalue":{"value":"28876","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7361808$BA118F9E-8CEA-460B-9EE8-FB565E6A8BC7","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"acf10290b955a69659a681d98822944f91bbad9e","datavalue":{"value":"68","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7361808$89251069-B676-4674-B6B2-ACBD64B961AF","rank":"normal"}],"P1458":[{"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":"Q7361808$C1E4D59E-053B-4B7B-B98D-AF85E4A921FA","rank":"normal"},{"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":"Q7361808$97F1D9B3-FC62-4DDE-BB74-EC93C2661EB7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"4dfac822d106dc7f697754008c4906d0b5156921","datavalue":{"value":{"entity-type":"item","numeric-id":35396,"id":"Q35396"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361808$25F8CD15-1C04-4B87-BEAF-158D8244AFC3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"6a1c834eaf7bf2e5bf95e7e5755a5eb5ec3363d0","datavalue":{"value":{"entity-type":"item","numeric-id":23493,"id":"Q23493"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361808$A3EFC373-3E5F-4C20-8A70-19DB27E19062","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"6d7523783c7058c43b9db4fb9e4c6275989a234b","datavalue":{"value":{"entity-type":"item","numeric-id":28682,"id":"Q28682"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361808$E23D69B5-C7A9-40B5-876C-EBC0DC9A5854","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"1c1111a4af73946d995c6025450c33305be35b38","datavalue":{"value":{"entity-type":"item","numeric-id":40350,"id":"Q40350"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361808$A65AF8FE-9609-434E-96A8-FC7DD4639DE0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"61d0c0612cc30c9c51b93ddaf1f78ee1ae75f9fe","datavalue":{"value":{"entity-type":"item","numeric-id":18676,"id":"Q18676"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361808$AD953C77-7089-4A0A-9B9F-925FEAE04A12","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"2ded5a481ece08049848bd1edb3f9afa21f0df2f","datavalue":{"value":{"entity-type":"item","numeric-id":16873,"id":"Q16873"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361808$66B8CB4E-BA7F-45BC-906B-88E7222CCDC4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"8dde418bf28e22fefe1976bd953eb7c8ec5b548d","datavalue":{"value":{"entity-type":"item","numeric-id":16770,"id":"Q16770"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361808$125DB420-FEE7-4DFD-9F20-A0AE87D341BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"f756f019005243c78675258773d8af1c07719cf8","datavalue":{"value":{"entity-type":"item","numeric-id":16615,"id":"Q16615"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361808$29EBCBDA-C0A0-42C3-B464-3032026CE0B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"b82152c1528c5be7e2040d1abd74977f4fe51817","datavalue":{"value":{"entity-type":"item","numeric-id":18672,"id":"Q18672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361808$D00AABE8-422F-4226-9EAD-8F9A158964B0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"cc4eff68b160f30b8d66dfcb610a0ea7a927079b","datavalue":{"value":{"entity-type":"item","numeric-id":17039,"id":"Q17039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361808$516F01E6-64ED-4999-BF11-850D09DE03A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"bfb5210bbde24d510bf39c9b54b7019412693a5b","datavalue":{"value":{"entity-type":"item","numeric-id":16825,"id":"Q16825"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361808$D89C6AA9-214D-46A7-89B1-3FD8F2717C41","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"6b90843c2343cce2fdb2e379b3e44155eedca437","datavalue":{"value":{"entity-type":"item","numeric-id":15028,"id":"Q15028"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361808$9DB78CC7-1DBE-49EC-9D8B-1FC675D1E028","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"2fd4f2f31989858180fba533a04e1a60c8d16377","datavalue":{"value":{"entity-type":"item","numeric-id":22154,"id":"Q22154"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361808$6C5A8303-CE22-40BE-B249-F3EACB38461C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"28fc316ccc1f38bd6830fcffe3187b6d32168084","datavalue":{"value":{"entity-type":"item","numeric-id":15455,"id":"Q15455"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361808$21454CF9-E462-4C4F-AE92-BA1022A31D41","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"144f0221487b5ba035abaca0f440960a9e47efeb","datavalue":{"value":{"entity-type":"item","numeric-id":27113,"id":"Q27113"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361808$F1697666-47F3-4E22-A27E-70E3DF36BB87","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"acf5d0da134f7563af94342a3a34b9ca28cd59db","datavalue":{"value":{"entity-type":"item","numeric-id":23989,"id":"Q23989"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361808$0DA972D2-A183-47B5-8888-050C64BE21D9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"632efb10a45ef079967d0b23f4dec91107ff81f2","datavalue":{"value":{"entity-type":"item","numeric-id":22241,"id":"Q22241"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361808$B88E2F6A-0A94-4BB6-A40E-1B0F5261C7E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a54e24244723bf29b2db533f355d939551876363","datavalue":{"value":{"entity-type":"item","numeric-id":22240,"id":"Q22240"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361808$B4241BD4-433C-4123-B840-4A2842EE1DFE","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Jinja is not Java","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Jinja_is_not_Java"}}}}}