Theses most similar to Using a denotational proof language to verify dataflow analyses (Hao, Melissa B. (Melissa Betty), 1979-; 2002) read it

Translating timed I/O automata specifications for theorem proving in PVs

Lim, Hongping (2006)

  • Advisor: Nancy A. Lynch
  • Department of Electrical Engineering and Computer Science
Read it

Metatheorems about convertibility in typed lambda calculi : applications to CPS transform and "free theorems"

Kuc̆an, Jakov (1997)

  • Advisor: Albert R. Meyer
  • Department of Mathematics
Read it

Denotational proof languages

Arkoudas, Konstantinos, 1968- (2000)

  • Advisor: Olin Shivers
  • Department of Electrical Engineering and Computer Science
Read it

Credible compilation

Marinov, Darko, 1976- (2000)

  • Advisor: Martin C. Rinard
  • Department of Electrical Engineering and Computer Science
Read it

Formal verification of simulations between I/O automata

Bogdanov, Andrej, 1978- (2001)

  • Advisor: Stephen J. Garland
  • Department of Electrical Engineering and Computer Science
Read it

Paired simulation of I/O automata

Ramírez-Robredo, J. Antonio (José Antonio), 1976- (2000)

  • Advisor: Nancy A. Lynch
  • Department of Electrical Engineering and Computer Science
Read it

A virtual machine for a type-[omega] denotational proof language

Arvizo, Teodoro, 1978- (2002)

  • Advisor: Howard E. Shrobe
  • Department of Electrical Engineering and Computer Science
Read it

A relatively small turing machine whose behavior is independent of set theory

Yedidia, Adam (2015)

  • Advisor: Scott Aaronson
  • Department of Electrical Engineering and Computer Science
Read it

Compilation using correct-by-construction program synthesis

Pit-Claudel, Clément (2016)

  • Advisor: Adam Chlipala
  • Department of Electrical Engineering and Computer Science
Read it

Eliminating intermediate lists in pH

Schwartz, Jacob B. (Jacob Benjamin), 1975- (2000)

  • Advisor: Arvind
  • Department of Electrical Engineering and Computer Science
Read it