Choose 6 of 7 questions below, and shuffle

  ***

1.3



2.1

Define some list operations and prove some lemmas on them.
  * concat
  * zip
  * product
  * upt
  * rotate1, rotate

2.2

Write inductive predicates specifying the following properties:

  * sortedness of lists
  * ...?

Prove that two characterizations of is_palindrome, in terms of reverse and an
inductive predicate, are the same.


2.3

Derive the >>= monadic laws from the >=> Kleisli laws

Use Kleisli to define mmap

Conversions between `do` and `>>=` notations


3.1

Prove program equivalences (optimizations) w.r.t. small- or big-step semantics:

  * seq (while b do c) (if b then c1 else c2)  ~  while b do c ; c2
  * seq (while true do c); c'  ~  while true do c
  * if b then while b do c else skip  ~  while b do c
  * while b do skip  ~  skip
  * if b then c1 else c2  ~  if ~ b then c2 else c1

Prove congruence rules:

  * if c ~ c', then  while b do c  ~~  while b do c'
  * if c1 ~ c1' and c2 ~ c2', then  if b then c1 else c2  ~  if b then c1' else c2'

Do-while language / Repeat language / For language

  * define syntax as inductive type
  * define big-step (or small-step) operational semantics
  * translate do-while to while, and prove equivalence
  * translate repeat language into if language
  * prove that all loop-free programs terminate

Transitive closure

  * let the students define various forms of closure (and inclusions)

  * three versions of the reflexive transitive closure (and variants, e.g. reflexive symmetric, etc.)
    * are they the same?
    * from transitive step, derive other two


3.2

One of the following two "consequence" rules is unsound. Use it to derive false.

Introduce a language construct, e.g. "unless", "do while", and give it a Hoare
rule (or choose among a list) -- prove it sound and complete?

Show a proof tree for the correctness of a simple program (without, then with
"while")


3.3

Define a denotational semantics (without `lfp`) of a constant-bounded repeat
language, and prove termination.

Relational denotational semantics the easy way, with reflexive transitive
closure, with a "loop" construct.


4.1

Quotient types:

  * finite multisets (from list)
  * finite sets (from list)

Subtypes:

  * sorted lists
  * finite set (from set)

Choice

  * Min (general), coincides with computational
  * Max on sets of nats

4.2

4.3


  ***
