Assignments

• A5. Due 5 Apr. Assignment description will given in lecture on 24 March.

• A4. Due 22 Mar. Use TulaFale to implement an abstracted variant of your web service for Assignment 2. Hopefully I will add more details later.

• A3. This is not really an assignment. Please download the following tools:
  • ProVerif
  • Samoa
  Try to familiarize yourself with the tools. Run some of the example protocols included in the distribution.

• A2. Due 15 Feb (Submit a URL and any supporting files by email): The purpose of this assignment is to create a simple web service. The functionality of the service is not important: it can be as simple as mapping the names of some of your imaginary friends to their phone numbers, or mapping simple arithmetic expressions to their values. Again feel free to use the software components of your choice and experiment with a few more advanced aspects (e.g., returning types other than the built-in XML types).

• A1. Due 27 Jan in class: Take all the examples in "The Essence of XML", transliterate them to actual XML/Schema, and check the matching and validation properties for each example using the tool of your choice.

Project Ideas

• TulaFale

  Use TulaFale to implement and verify an interesting web service.

• Behavioral Equivalence (for the mathematically-inclined)

  Research the various notions of behavioral equivalences for some simple variant of the pi-calculus. Write a summary of your findings. Include some examples and outline the proof for proving at least one of the equivalences you discuss.

• Process Calculi and Security Protocols

  Use a language based on one of the process calculi (e.g, PICT, JoCaml, LySa) and implement a few security protocols.

• Continuations and Web Servers

  Research the use of continuations in web servers. Write a description of the problems that continuations are supposed to solve, how well they solve them, and what are the problems associated with the use of continuations. Support your narrative with code (or pseudo-code) from a web server implemented using continuations.

• XML Processing

  Design or find an interesting (non-trivial) XML document format. Use XDuce (or a similar typed XML processing language) to write a few programs that process your documents.

• XML (Implementation)

  Part I: Take the subset of XML values and schemas introduced in "The Essence of XML" and implement matching, erasure, validation, and optimized matching.

  Part II: Extend your implementation with at least one additional construct from the full XML/Schema definition.

• XML (Proofs)

  Prove the two main theorems in "The Essence of XML:" Validation (Theorem 1), Sensibility (Theorem 2).

Presentations