Paper Library

This is a simple imperative language with numbers and Booleans. Additionally, one extension adds a new analysis to determine if a program can leak private information.

This is the example from our paper, "A Modular Approach to Metatheoretic Reasoning for Extensible Languages".

• Host language: Simple imperative language with numbers and records
• Security extension: Adds an analysis to determine if a program can leak private information
• List extension: Adds syntax for list expressions

Download example tarball

Back to examples