天宇陈

我是一个博士生在布卢明顿市印第安纳大学计算机科学教授的建议雷竞技官方网站下载杰里米·g·Siek。

我喜欢建筑机械化证明和形式化的编程语言证明助理。我最近的工作重点是推理逐渐类型语言,一些类型的信息是静态未知,和它们的属性建模Agda。

我是一个实习生在软件验证CertiK在2021年夏天。我从事认证系统软件的功能正确性使用公鸡和CompCert。

我组织的编程语言阅读小组(PLRG@IU)。请参考我们的网站如果你有兴趣参加!随时给我发电子邮件,如果你有问题。

• 机械化逐步安全不干扰新!
  天宇,杰里米·g·Siek
  在草案提交
  ArxivPDF代码
• 参数化结石和可重用Meta-theory对于逐渐类型λ结石
  杰里米·g . Siek天宇
  杂志的函数式编程
  DOIArxiv代码
• 机械化逐步信息流的类型安全
  天宇,杰里米·g·Siek
  LangSec 2021
  DOIPDF说话幻灯片代码
• 赛车在多维空间:关闭超线程侧通道在新交所的数据竞争
  天宇Guoxing Chen朱文昊Wang Chen,三川Chen Yinqian张XiaoFeng Wang Ten-Hwang Lai Dongdai林
  2018年IEEE安全和隐私
• 描述Smartwatch在野外使用
  邢Liu天宇,冯钱Zhixiu郭,菲利克斯Xiaozhu Lin Xiaofeng Wang Kai陈
  2017年经验
• Paxos做成透明的
  赫明崔,鲁伊·顾,程Liu天宇Chen Junfeng杨
  SOSP 2015

• 通用Blame-Subtyping定理Agda使用抽象绑定树
  天宇陈
  选择参与POPL 2022学生研究竞争
  扩展的抽象海报

• 雷竞技官方网站下载印第安纳大学校历链接
• Spacemacs Agda层链接

• 电子邮件:\ (\ mathtt {chen512} @ \ mathtt{印第安纳}。\ mathtt {edu} \)
• 办公室:小隔间3025 b。Luddy大厅,印第安纳雷竞技官方网站下载大学。n .据大道700号的布卢明顿在47408年

• 这一页是写的org-mode和发布到HTML。