{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,3]],"date-time":"2026-04-03T22:41:35Z","timestamp":1775256095028,"version":"3.50.1"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319980461","type":"print"},{"value":"9783319980478","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-98047-8_17","type":"book-chapter","created":{"date-parts":[[2018,10,23]],"date-time":"2018-10-23T21:05:49Z","timestamp":1540328749000},"page":"267-282","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Illi Isabellistes Se Custodes Egregios Praestabant"],"prefix":"10.1007","author":[{"given":"Simon","family":"Bischof","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joachim","family":"Breitner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Denis","family":"Lohner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gregor","family":"Snelting","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,10,24]]},"reference":[{"key":"17_CR1","doi-asserted-by":"publisher","unstructured":"Simon Bischof et al. \u201cLow-Deterministic Security For Low-Deterministic Programs\u201d. In: Journal of Computer Security 26 (2018), pp. 335\u2013336. https:\/\/doi.org\/10.3233\/JCS17984","DOI":"10.3233\/JCS17984"},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"Joachim Breitner. \u201cFormally proving a compiler transformation safe\u201d. In: Proceedings of the 8th ACM SIGPLAN Symposium on Haskell, Haskell 2015, Vancouver BC, Canada, September 3\u20134, 2015. 2015, pp. 35\u201346.","DOI":"10.1145\/2804302.2804312"},{"key":"17_CR3","unstructured":"Joachim Breitner. \u201cLazy Evaluation: From natural semantics to a machine-checked compiler transformation\u201d. PhD thesis. Karlsruher Institut f\u00fcr Technologie, Fakult\u00e4t f\u00fcr Informatik, Apr. 2016."},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"Joachim Breitner. \u201cThe adequacy of Launchbury\u2019s natural semantics for lazy evaluation\u201d. In: J. Funct. Program. 28 (2018), e1. https:\/\/doi.org\/10.1017\/S0956796817000144 .","DOI":"10.1017\/S0956796817000144"},{"key":"17_CR5","unstructured":"Joachim Breitner. \u201cThe Correctness of Launchbury\u2019s Natural Semantics for Lazy Evaluation\u201d. In: Archive of Formal Proofs (Jan. 2013). ISSN: 2150-914x. http:\/\/afp.sf.net\/entries\/Launchbury.shtml ."},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"Joachim Breitner. \u201cThe Safety of Call Arity\u201d. In: Archive of Formal Proofs (Feb 2015).","DOI":"10.1007\/978-3-319-14675-1_3"},{"key":"17_CR7","doi-asserted-by":"crossref","unstructured":"Joachim Breitner et al. \u201cOn Improvements Of Low-Deterministic Security\u201d. In: Proc. Principles of Security and Trust (POST) Ed. by Frank Piessens and Luca Vigan\u00f2. Vol. 9635. Lecture Notes in Computer Science. Springer Berlin Heidelberg, 2016, pp. 68\u201388.","DOI":"10.1007\/978-3-662-49635-0_4"},{"key":"17_CR8","unstructured":"Pablo Buiras and Alejandro Russo. \u201cLazy Programs Leak Secrets\u201d. In: NordSec Vol. 8208. Lecture Notes in Computer Science. Springer, 2013, pp. 116\u2013122."},{"key":"17_CR9","unstructured":"Dennis Giffhorn. \u201cSlicing of Concurrent Programs and its Application to Information Flow Control\u201d. PhD thesis. Karlsruher Institut f\u00fcr Technologie, Fakult\u00e4t f\u00fcr Informatik, May 2012."},{"issue":"3","key":"17_CR10","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/s10207-014-0257-6","volume":"14","author":"Dennis Giffhorn","year":"2014","unstructured":"Dennis Giffhorn and Gregor Snelting. \u201cA New Algorithm For Low-Deterministic Security\u201d. In: International Journal of Information Security 14.3 (Apr 2015), pp. 263\u2013287.","journal-title":"International Journal of Information Security"},{"key":"17_CR11","unstructured":"J\u00fcrgen Graf. \u201cInformation Flow Control with System Dependence Graphs \u2014 Improving Modularity Scalability and Precision for Object Oriented Languages\u201d. PhD thesis. Karlsruher Institut f\u00fcr Technologie, Fakult\u00e4t f\u00fcr Informatik, 2016."},{"key":"17_CR12","unstructured":"J\u00fcrgen Graf et al. \u201cTool Demonstration: JOANA\u201d. In: Proc. Principles of Security and Trust (POST) Ed. by Frank Piessens and Luca Vigan\u00f2. Vol. 9635. Lecture Notes in Computer Science. Springer Berlin Heidelberg, 2016, pp. 89\u201393."},{"issue":"6","key":"17_CR13","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1007\/s10207-009-0086-1","volume":"8","author":"Christian Hammer","year":"2009","unstructured":"Christian Hammer and Gregor Snelting. \u201cFlow-Sensitive, Context-Sensitive, and Object- sensitive Information Flow Control Based on Program Dependence Graphs\u201d. In: Interna- tional Journal of Information Security 8.6 (Dec. 2009), pp. 399\u2013422.","journal-title":"International Journal of Information Security"},{"key":"17_CR14","volume-title":"Construction and Stochastic Applications of Measure Spaces in Higher Order Logic","author":"Johannes H\u00f6lzl","year":"2013","unstructured":"Johannes H\u00f6lzl. \u201cConstruction and Stochastic Applications of Measure Spaces in Higher Order Logic\u201d. Dissertation. M\u00fcnchen: Technische Universit\u00e4t M\u00fcnchen, 2013."},{"key":"17_CR15","doi-asserted-by":"crossref","unstructured":"Ralf K\u00fcsters et al. \u201cExtending and Applying a Framework for the Cryptographic Verification of Java Programs\u201d. In: Proc. POST 2014 LNCS 8424. Springer, 2014, pp. 220\u2013239.","DOI":"10.1007\/978-3-642-54792-8_12"},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"John Launchbury \u201cA Natural Semantics for Lazy Evaluation\u201d. In: Principles of Programming Languages (POPL) ACM, 1993. DOI: 10.1145\/158511.158618.","DOI":"10.1145\/158511.158618"},{"key":"17_CR17","unstructured":"Andreas Lochbihler \u201cA Machine-Checked, Type-Safe Model of Java Concurrency : Language, Virtual Machine, Memory Model, and Verified Compiler\u201d. PhD thesis. Karlsruher Institut f\u00fcr Technologie, Fakult\u00e4t f\u00fcr Informatik, July 2012."},{"key":"17_CR18","doi-asserted-by":"crossref","unstructured":"Andreas Lochbihler. \u201cMaking the Java Memory Model Safe\u201d. In: ACM Transactions on Programming Languages and Systems 35.4 (2014), 12:1\u201312:65.","DOI":"10.1145\/2518191"},{"key":"17_CR19","doi-asserted-by":"crossref","unstructured":"Andreas Lochbihler. \u201cVerifying a Compiler for Java Threads\u201d. In: Proc. 19th European Symposium on Programming ESOP 2010 Vol. 6012. Lecture Notes in Computer Science. 2010, pp. 427\u2013447.","DOI":"10.1007\/978-3-642-11957-6_23"},{"issue":"02","key":"17_CR20","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1017\/S0956796800000319","volume":"2","author":"Simon L. Peyton Jones","year":"1992","unstructured":"Simon Peyton Jones. \u201cImplementing Lazy Functional Languages on Stock Hardware: The Spineless Tagless G-Machine\u201d. In: Journal of Functional Programming 2.2 (1992), pp. 127\u2013202. https:\/\/doi.org\/10.1017\/S0956796800000319 .","journal-title":"Journal of Functional Programming"},{"key":"17_CR21","unstructured":"Andrew M. Pitts. \u201cNominal logic, a first order theory of names and binding\u201d. In: Theoretical Aspects of Computer Software (TACS) 2001 Vol. 186. Information and Computation 2. Elsevier, 2003, pp. 165\u2013193. https:\/\/doi.org\/10.1016\/S08905401(03)00138X"},{"key":"17_CR22","unstructured":"Andrei Popescu, Johannes H\u00f6lzl, and Tobias Nipkow. \u201cFormal Verification of Language- Based Concurrent Noninterference\u201d. In: J. Formalized Reasoning 6.1 (2013), pp. 1\u201330."},{"key":"17_CR23","unstructured":"Andrei Popescu, Johannes H\u00f6lzl, and Tobias Nipkow \u201cFormalizing Probabilistic Nonin- terference\u201d. In: Proc. Certified Programs and Proofs CPP Vol. 8307. Lecture Notes in Computer Science. 2013, pp. 259\u2013275."},{"key":"17_CR24","doi-asserted-by":"crossref","unstructured":"Andrei Popescu, Johannes H\u00f6lzl, and Tobias Nipkow. \u201cNoninterfering Schedulers When Possibilistic Noninterference Implies Probabilistic Noninterference\u201d. In: Proc. Algebra and Coalgebra in Computer Science (CALCO) Lecture Notes in Computer Science. 2013, pp. 236\u2013252.","DOI":"10.1007\/978-3-642-40206-7_18"},{"issue":"1","key":"17_CR25","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1109\/JSAC.2002.806121","volume":"21","author":"A. Sabelfeld","year":"2003","unstructured":"A. Sabelfeld and A. Myers. \u201cLanguage-Based Information-Flow Security\u201d. In: IEEE Journal on Selected Areas in Communications 21.1 (Jan. 2003), pp. 5\u201319.","journal-title":"IEEE Journal on Selected Areas in Communications"},{"key":"17_CR26","doi-asserted-by":"crossref","unstructured":"Andrei Sabelfeld and David Sands. \u201cProbabilistic Noninterference for Multi-Threaded Programs\u201d. In: Proceedings of the 13th IEEE Computer Security Foundations Workshop, CSFW \u201900, Cambridge England, UK, July 3\u20135, 2000. 2000, pp. 200\u2013214.","DOI":"10.1109\/CSFW.2000.856937"},{"key":"17_CR27","unstructured":"Lidia S\u00e1nchez-Gil, Mercedes Hidalgo-Herrero, and Yolanda Ortega-Mall\u00e9n. \u201cLaunchbury\u2019s semantics revisited: On the equivalence of context-heap semantics (Work in progress)\u201d. In: XIV Jornadas sobre Programaci\u00f3n y Lenguajes (2014), pp. 203\u2013217."},{"key":"17_CR28","doi-asserted-by":"crossref","unstructured":"Lidia S\u00e1nchez-Gil, Mercedes Hidalgo-Herrero, and Yolanda Ortega-Mall\u00e9n. \u201cRelating func- tion spaces to resourced function spaces\u201d. In: Symposium on Applied Computing (SAC) ACM, 2011, pp. 1301\u20131308. https:\/\/doi.org\/10.1145\/1982185.1982469","DOI":"10.1145\/1982185.1982469"},{"key":"17_CR29","unstructured":"Lidia S\u00e1nchez-Gil, Mercedes Hidalgo-Herrero, and Yolanda Ortega-Mall\u00e9n. \u201cThe role of indirections in lazy natural semantics\u201d. In: Perspectives of System Informatics (PSI) 2014 Vol. 8974. LNCS. Springer, 2015. https:\/\/doi.org\/10.1007\/9783662468234<currencydollar>backslash<currencydollar>textunderscore24"},{"key":"17_CR30","doi-asserted-by":"crossref","unstructured":"Gregor Snelting. \u201cPaul Feyerabend and software technology\u201d. In: International Journal on Software Tools for Technology Transfer 2.1 (Nov 1998), pp. 1\u20135.","DOI":"10.1007\/s100090050013"},{"key":"17_CR31","doi-asserted-by":"crossref","unstructured":"Gregor Snelting. \u201cPaul Feyerabend und die Softwaretechnologie\u201d. In: Informatik-Spektrum 21.5 (Oct. 1998), pp. 273\u2013276.","DOI":"10.1007\/s002870050105"},{"key":"17_CR32","unstructured":"Christian Urban and Cezary Kaliszyk. \u201cGeneral Bindings and Alpha-Equivalence in Nominal Isabelle\u201d. In: Logical Methods in Computer Science 8.2 (2012). DOI: 10.2168\/LMCS8(2: 14)2012."},{"key":"17_CR33","unstructured":"Daniel Wasserrab. \u201cFrom Formal Semantics to Verified Slicing \u2013 A Modular Framework with Applications in Language Based Security\u201d. PhD thesis. Karlsruher Institut f\u00fcr Technologie, Fakult\u00e4t f\u00fcr Informatik, Oct. 2010. http:\/\/digbib.ubka.uni-karlsruhe.de\/volltexte\/1000020678 ."},{"key":"17_CR34","unstructured":"Daniel Wasserrab. \u201cInformation Flow Noninterference via Slicing\u201d. In: Archive of Formal Proofs (2010)."},{"key":"17_CR35","doi-asserted-by":"crossref","unstructured":"Daniel Wasserrab, Denis Lohner, and Gregor Snelting. \u201cOn PDG-Based Noninterference and its Modular Proof\u201d. In: Proc. PLAS \u201909 ACM. Dublin, Ireland, June 2009. http:\/\/pp.info.unikarlsruhe.de\/uploads\/publikationen\/wasserrab09plas.pdf .","DOI":"10.1145\/1554339.1554345"},{"key":"17_CR36","doi-asserted-by":"crossref","unstructured":"Daniel Wasserrab et al. \u201cAn Operational Semantics and Type Safety Proof for Multiple Inheritance in C+\u2009+\u201d. In: 21th Annual ACM Conference on Object-Oriented Programming Systems, Languages, and Applications ACM, Oct. 2006, pp. 345\u2013362.","DOI":"10.1145\/1167473.1167503"},{"key":"17_CR37","doi-asserted-by":"crossref","unstructured":"Steve Zdancewic and Andrew C. Myers. \u201cObservational Determinism for Concurrent Pro- gram Security\u201d. In: Proc. CSFW. IEEE, 2003, pp. 29\u201343.","DOI":"10.1109\/CSFW.2003.1212703"}],"container-title":["Principled Software Development"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-98047-8_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,3]],"date-time":"2026-04-03T21:20:40Z","timestamp":1775251240000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-98047-8_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319980461","9783319980478"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-98047-8_17","relation":{},"subject":[],"published":{"date-parts":[[2018]]}}}