![Yann Herklotz](https://pldi22.sigplan.org/getProfileImage/yannherklotz/4a59aa07-d177-4b5e-8a42-1284513f17e0/small.jpg?1711546212000)
Registered user since Wed 12 Jun 2019
Name:Yann Herklotz
Bio:
My research focuses on formalising the process of converting high-level programming language descriptions to correct hardware that is functionally equivalent to the input. This process is called high-level synthesis (HLS), and allows software to be turned into custom accelerators automatically, which can then be placed on field-programmable gate arrays (FPGAs). An implementation in the Coq theorem prover called Vericert can be found on Github.
Country:United Kingdom
Affiliation:Imperial College London
Personal website: https://yannherklotz.com
X (Twitter): https://x.com/ymherklotz
GitHub: https://github.com/ymherklotz
Research interests:Theorem Proving, High-Level Synthesis, Hardware
Contributions
PLDI 2022-profile
View general profile
View general profile