Hi there! I am Shriya, a student studying Math and Computer Science. I am interested in the study of Programming Languages and Verification, including their theory, semantics, design, and implementation, with a focus on types and type Systems.
In particular, I am interested in Functional languages and their type systems and am currently working on dependently typed languages in order to one day extend it to support dependent-intersection types.
For some of of you who maybe new here, dependent-intersection types are a special way to encode a multitude of types namely inductive-inductive and inductive-recursive without changing the core of the language. I am trying to see if there is a simple way to construct this type by extending plain old sigma (or dependent) types.
A thorough explanation with example of dependent intersection types is mentioned in the pdf attached
- In the functional realm, I have experience coding in Haskell, OCaml, and Ruby.
- In the object oriented realm I have experience coding in C/C++, Python, and Java
- In the dependent realm I have experience with Coq (pronounced coke), Agda, and EasyCrypt.
- 📫 I can be reached on shriyacool23@gmail.com