Lars Warren Ericson, PhD
I earned my PhD from the Courant Institute Computer Science
Department in 1994.
My PhD thesis was on some pragmatic issues
related to the application of decidable sublanguages
of set theory to the derivation of correct programs.
Press here for a .PDF copy of my PhD thesis.
My advisor was Bud
Cox and Ed
Schonberg were my co-advisors.
In my Ph.D thesis, I
For further information on my current career, please see my LinkedIn profile.
Implemented in Mathematica a version
Schwartz's "programs with assumptions and assertions" (PRAA) proof
system for deriving correct set operation-oriented programs. PRAA's were
the framework for their "Correct Program Technology" research initiated
around 1975. For this effort Prof. Schwartz and his colleagues also developed
decision procedures for about 25 different sublanguages of set theory,
to be used as "one step" proof rules for a SETL-like target language. The
worst-case complexity of these procedures led me to consider the (separate)
topics of simplication rules (a.k.a "heuristics") and the average-case
complexity of decision procedures in logic.
Computed the applicability (in terms of number of matches for the number
of expressions involving a certain number of variables) of some kinds of
simplification rules for set expressions.
- Reviewed what was known about the average case complexity of decision
procedures for set expressions. The review of average case complexity is
available on-line as the NYU CSD Tech Report
Cox, Ericson and Mishra, 1995.