ice1000

Pennsylvania, USA

https://ice1000.org

I'm into univalent type systems. Worked on Agda and Arend, looking for PhD or similar research position.

Profile: https://personal.psu.edu/yqz5714

top accounts reputation activity subscriptions

Why do some PL choose to have a dedicated keyword for elseif instead of like in C?

syntax language-comparison asked May 16, 2023 at 17:16

langdev.stackexchange.com

36 votes

How to implement this Java interface in Kotlin?

java kotlin kotlin-interop asked May 23, 2017 at 10:44

stackoverflow.com

30 votes

What is an algebraic data type?

terminology algebraic-data-types asked Feb 27, 2022 at 21:58

proofassistants.stackexchange.com

21 votes

Are implicit arguments essential to (dependently-typed) proof assistants?

implicit-argument asked Feb 8, 2022 at 18:16

proofassistants.stackexchange.com

21 votes

What's the difference between reflection and tactics?

tactic reflection asked Mar 19, 2022 at 20:29

proofassistants.stackexchange.com

18 votes

How much of trouble is Lean's failure of normalization, given that logical consistency is not obviously broken?

lean normalization asked Mar 27, 2022 at 20:07

proofassistants.stackexchange.com

18 votes

Is internal parametricity useful in theorem proving?

parametricity asked Feb 9, 2022 at 12:19

proofassistants.stackexchange.com

18 votes

What are the advantages of normalization by evaluation over traditional reduction-based normalization?

normalization asked Feb 9, 2022 at 15:03

proofassistants.stackexchange.com

17 votes

What are the pros and cons of eliminators vs. pattern matching with a termination checker?

types asked May 16, 2023 at 20:49

langdev.stackexchange.com

16 votes

What happened to Conor McBride's universe polymorphism proposal?

universe-polymorphism asked Feb 9, 2022 at 1:46

proofassistants.stackexchange.com

Top Answers

What are different ways of handling runtime errors?

langdev.stackexchange.com

IntelliJ: changing color of an unused variable

stackoverflow.com

What are the drawbacks of using indentation for code blocks?

langdev.stackexchange.com

How to apply a patch generated with git format-patch?

stackoverflow.com

Is there Multimap in Kotlin?

stackoverflow.com

Why do some languages have quotes around imports?

langdev.stackexchange.com

What are the drawbacks of using indentation for code blocks?

langdev.stackexchange.com

What is implied by the names "sum type" and "product type"?

langdev.stackexchange.com

In Agda, why is universe polymorphism explicit?

proofassistants.stackexchange.com

What is the difference between judgmental equality, definitional equality, and equality types?

proofassistants.stackexchange.com

What does Kotlin's type reification make possible that is not possible in Java or Scala?

stackoverflow.com

What are some syntax options for describing generic ("templated") types?

langdev.stackexchange.com

Android Kotlin View width set error "Val cannot be reassigned"

stackoverflow.com

How to use annotation TypeDefs in Kotlin?

stackoverflow.com

How to organize Kotlin extension methods

stackoverflow.com

Are there any proof assistants which integrate JITs?

proofassistants.stackexchange.com

What are the differences between MLTT and CIC?

proofassistants.stackexchange.com

How to check "instanceof " class in Kotlin?

stackoverflow.com

How would a Kotlin notebook work when kotlin is a compiled language?

stackoverflow.com

Equivalent of Java's 'public static final string'

stackoverflow.com

Why is cumulativity not a given in proof assistants?

proofassistants.stackexchange.com

Have ideas from programming helped us create new mathematical proofs?

proofassistants.stackexchange.com

How might one formally communicate/define/describe a programming language design?

langdev.stackexchange.com

How to create real static property in kotlin

stackoverflow.com

How to fix conflicting Kotlin dependency in IntelliJ IDEA?

stackoverflow.com

Is there a way to automatically translate proofs from one proof assistant to another?

proofassistants.stackexchange.com

How to convert char to ascii value in kotlin language

stackoverflow.com

Kotlin internal classes in Java visible publicly

stackoverflow.com

Kotlin auto complete overrides in Android Studio

stackoverflow.com

Why care about consistency?

langdev.stackexchange.com