I recently decided to go back to college when I realized that having all of the certifications and work experience in the world wasn't going to do me any good unless I had a decent formal education.
During my 3 year stint in academia I have acquired up a double B.S. in Mathematics and Computer Science, an M.A. in Mathematics, and a Graduate Certificate in Artificial Intelligence. I am now a thesis away from my M.S. in Computer Science, and a class or two from a Graduate Certificate in Bioinformatics, should I decide to pursue it. I've maintained a 4.0 GPA, and double honors.
I am employed at Eastern Michigan University as an adjunct lecturer in the Computer Science Department and as a programmer for the Institute for Language Information Technology, the new parent organization over the LINGUIST List. I am currently working on the interfaces for the LL-Map and Multitree projects.
My current thesis involves employing the Curry-Howard-de Bruijn correspondence on an extended lattice of substructural logics to construct and implement an intermediate representation for compiling functional programming languages. My approach highlights the distinction between linear logic of Jean-Yves Girard and uniqueness type systems used in programming languages such as Clean. In the interest of freeing the intermediate representation from the vagaries of strict vs. lazy evaluation, I am working in a calculus with an explicit value-continuation duality. However, such a calculus isn't very interesting until it is extended with the various features modern functional programmers expect in a language. To that end I have been constructing a variant form of a pure type systems with subtyping that can be constructed over a fully continuation passing style transformed calculus. Since my substructural types include ordered continuations, the CPS transformation yields, somewhat-paradoxically, a nice stack model. The resulting system extends a basic system that can be shown sound and strongly normalizing for a wide class of substructural type lattices by appealing to the universal cut-elimination theorem for Nuel Belnap's display logic.
This has distant ties to linguistics since one of the weakest logics in the arsenal was defined by Jim Lambek. By combining the extended lattice of substructural types with linear region-based memory management the resulting system can help functional programming languages achieve better performance without ad hoc passes for strictness analysis and without the wasted memory usually associated with region-based memory management.
My compiler is currently being designed to target the x86-64 architecture to take advantage of reduced register pressure and the additional optimizations that can be performed knowing the structure of my types. At a low level, I am interested in finding and exploiting opportunities for SIMD superword-level parallelism in functional programs and examining region-based register allocation and extended notions of principal type inference to help perform a number of analyses as a side-effect of the compilation process. At a higher level, I am interested in exploring the design space to figure out what a useful functional programming language designed for data parallelism and substructural typing should look like.
My mathematics thesis covered the adaptation of an 130-year old coordinate system designed by Eduard Study for lines and their duals to Jorge Stolfi's oriented projective geometry. Once adapted it is quite useful when working with transversal problems in 3D scenes. Computer Scientists like to call these “stabbing line problems.” Study's coordinates have some nice properties that occasionally makes them a useful basis in which to express the points in P5 that lie on the Plücker quadric, or as it is also known, the Grassmannian Manifold F24. Points on this quadric can be used to represent lines in P3 in a homogeneous manner that is conducive to determining visible surfaces and calculating occlusion. This is an extension of my earlier obsession with 3D graphics, which led to a series of articles called "Harmless Algorithms" for a now-defunct gaming site, flipCode.
Linguistically, as I am mostly an outsider my interests are more mainstream: Minimalist Syntax and Computational Linguistics.
It is my intention to disseminate my programming experience among my coworkers here at LINGUIST, while I in turn learn more about Linguistics.
-Edward A. Kmett