->Main   
 
->Research   
 
->Interests   
 
->Life   
 
->Random   
 
->Hebrew   
 
->Bookmarks   
 
->Meaning   
 

Research

--------------------

PLT Scheme

I am now part of the PLT Scheme group, the Northeastern branch.

Reflection

I have worked on an implementation of practical reflection for Nuprl.
  • The "Reflection" theory is accessible in this automatically-generated PostScript file.
  • An example of using it is a formalization of the Tarski argument about the undefinability of truth.
  • The HOAS representation is described in "Reflecting Higher-Order Abstract Syntax in Nuprl" [PostScript] [PDF].
  • My thesis is available too.

BOOMS

As part of my master thesis I implemented Booms: a structure editor for music.