Alexander Altman
I am a Master's Student at the University of Illinois, Urbana-Champaign; I earned my B.S. in Computer Science from California State University, Stanislaus.
My primary research focus is in locational type theory, a generic framework for combining modal and stratified logics using the power of dependent type theory. My other research interests include language design for practical encoding of underrepresented paradigms (such as the Entity-Component-System organizational paradigm, the native-structure/path-oriented data-design paradigm, or the “wisp-based” concurrency paradigm), as well as other extensions to dependent type theory (such as very dependent functions and very (co)inductive types, or confluent multiple elimination).
Locational Type Theory (LoTT)
The key insight of LoTT is that modal structures of unlimited complexity can be represented as ordinary types in Martin-Löf dependent type theory (MLTT); therefore, introducing a mechanism for lifting values of a selected type into the layer of contexts as an extensible stratification operator suffices to encode any arbitrary modality and/or stratification system in otherwise unaltered MLTT.
Preliminary results suggest that LoTT is capable of usefully representing and working with temporal, spatial, doxastic, epistemic, assumptive, phasal, and even more exotic modal logics, as well as (possibly dependent) products and sums of them in a natural, freely-generated way.