净土

Zhang Tesla

ice1000

注册于 12/10/2017, 1:53:09 AM

Programming for interest. https://personal.psu.edu/yqz5714 and https://ice1000.org are my websites

它的提问

Elaborating Dependent Copattern Matching 中到底有几颗AST？

9/17/2019, 3:02:49 PM

为什么 Path type 不能是 Pi type 的 subtype？

9/17/2019, 3:02:35 PM

Fraïssé Theorem 和 Univalence Axiom 形式类似，他们有什么异同？

9/17/2019, 3:02:21 PM

如何理解 Cartesian Cubical TT 中的 V type？

9/17/2019, 3:01:51 PM

Row polymorphism的实现有什么好的阅读材料？

6/2/2019, 2:51:12 AM

为什么我只能看最近的一些问题？

6/2/2019, 1:35:08 AM

HOL 的【AI】是什么东西？

5/31/2019, 9:30:40 PM

如何评价MiniAgda编程语言？

5/29/2019, 5:26:05 PM

Dependent Type 语言一般会设计哪几层AST？

5/27/2019, 3:02:09 PM

TiKV 的 client 有哪些实际用途，以及未来可能出现但现在还不支持的功能？

5/27/2019, 2:57:37 PM

如何评价 TiDB 数据迁移工具： TiDB-Lightning？

5/27/2019, 2:55:59 PM

如何评价大学还在生活上接受父母照顾的人？

5/26/2019, 2:53:33 AM

Dependent Type的Core Language中Lambda一般都不存参数类型，为什么我们可以这么做？

5/26/2019, 2:48:56 AM

如何评价 TiKV 子项目 Titan，分离 RocksDB 中存储的大型数据？

5/23/2019, 9:34:41 PM

基于 Sized Types 的 termination check 有优化空间吗？

5/23/2019, 9:30:58 PM

Cubical Type Theory 还有什么可以进一步发展的地方？

5/23/2019, 9:26:13 PM

如何评价 IntelliJ 即将推出的官方 shell 插件？

5/23/2019, 9:13:21 PM

MiniAgda的ScopeChecker和TypeChecker是分离的，如何评价这种做法？

5/22/2019, 3:08:07 PM

是什么在驱动HOL的长期开发？

5/22/2019, 3:06:20 PM

JetBrains Research除了Arend之外还在做什么？

5/22/2019, 3:04:39 PM