smooththunk Goto Github PK

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 [email protected]