Skip to content
View Hughshine's full-sized avatar
🧿
Focusing
🧿
Focusing
Block or Report

Block or report Hughshine

Block user

Prevent this user from interacting with your repositories and sending you notifications. Learn more about blocking users.

You must be logged in to block users.

Please don't include any personal information such as legal names or email addresses. Maximum 100 characters, markdown supported. This note will be visible to only you.
Report abuse

Contact GitHub support about this user’s behavior. Learn more about reporting abuse.

Report abuse
Hughshine/README.md

Hi there 👋 Blessing on your day.

I'm Xuyang Li, currently a postgraduate student majoring in computer science at Nanjing University. Feel free to chat with me at xuyang.li at smail dot nju dot edu dot cn!

I research on formal methods and software engineering techiques. I'm also interested in humanity (cultural aspects) and human-computer interface, creating functional and immersive softwares (or say, "art", :D) to support, expand and enrich human's perceptions and experiences within this universe.

For former projects, I've worked on verified compilation (see CompCert) and polyhedral compilation (see Pluto). I also know something about relaxed concurrency (see compiler verification on Promising Semantics). I mechanize proofs with Coq proof assistant.

If you're interested, just drop by my homepage!

2023.10.11

Pinned

  1. verif-scop/PolCert verif-scop/PolCert Public

    A verified polyhedral scheduling validator in Coq.

    Coq 17 1

  2. promising-comp promising-comp Public

    Mirror for compcert implementation in promising semantics

    Coq

  3. bondhugula/pluto bondhugula/pluto Public

    Pluto: An automatic polyhedral parallelizer and locality optimizer

    C 248 64

  4. AbsInt/CompCert AbsInt/CompCert Public

    The CompCert formally-verified C compiler

    Coq 1.8k 218