Toward Type-Preserving Compilation of Coq
I am a fifth year Ph.D. student at Northeastern University where I study Computer Science (specifically, programming languages).
The promise of programming languages research has been to provide high-level languages in which programmers can easily write complex programs without worrying about speed or low-level machine details. I think we have failed. Languages that provide strong guarantees are bemoaned as too complicated, compilers ignore those high-level guarantees anyway, and the folklore persists that C is the only language useful for writing fast code.
I want to make programs easier to design, write, and understand. To that end, I work on verifying compilers. I am particularly interested in equivalence preserving (fully-abstract) compilers. I also dabble in dependent types and compiler design and implementation.
Thu 19 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
18:20 - 20:20 | Poster SessionStudent Research Competition at Auditorium Hall Chair(s): Matteo Cimini Indiana University, USA, Kim Nguyễn LRI, Université Paris-Sud, Julien Signoles CEA LIST, Qirun Zhang University of California, Davis | ||
18:20 10mDemonstration | Naturality despite Nontermination: A Logical Relation for Linear Types and Polymorphism Student Research Competition Nicholas Rioux Northeastern University | ||
18:30 10mDemonstration | Gradual Type Precision as Retraction Student Research Competition Max S. New Northeastern University | ||
18:40 10mDemonstration | Linking Types: Specifying Safe Interoperability and Equivalences Student Research Competition Daniel Patterson Northeastern University | ||
18:50 10mDemonstration | A Monadic Framework for Bidirectional Programming Student Research Competition Li-yao Xia ENS Paris | ||
19:00 10mDemonstration | Gradual Set-Theoretic Types Student Research Competition Victor Lanvin ENS Paris-Saclay | ||
19:10 10mDemonstration | Abstract Interpretation of High-Level Transformations Student Research Competition Ahmad Salim Al-Sibahi IT University of Copenhagen, Denmark | ||
19:20 10mDemonstration | FairSquare: A Static Analysis Tool for Algorithmic Fairness Student Research Competition Samuel Drews University of Wisconsin-Madison | ||
19:30 10mDemonstration | Toward Type-Preserving Compilation of Coq Student Research Competition William J. Bowman Northeastern University | ||
19:40 10mDemonstration | A Symbolic Execution Framework for Haskell Student Research Competition Anton Xue Yale University | ||
19:50 10mDemonstration | Synthesizing Imperative Programs from Examples for Introductory Programming Assignments Student Research Competition Sunbeom So Korea University | ||
20:00 10mDemonstration | Provenance for Configuration Language Security Student Research Competition Weili Fu University of Edinburgh | ||
20:10 10mDemonstration | A gradually typed polymorphic lambda calculus Student Research Competition Yuu Igarashi Kyoto University | ||
