Area 51 » ice1000

info activity reputation

reputation

124 views

discussion user

network profile

Registered User

name	ice1000
member for	2 years
seen	May 2 at 20:21
website	ice1000.org
location	Pennsylvania, USA

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

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

stats accounts

0

Proposals

0

Current Commitments

2

Fulfilled Commitments

970

days

Proof Assistants

For mathematicians and computer scientists who develop and use proof assistants.

define

commit

public beta

508

days

Programming Language Design and Implementation

For designers and implementers of computer programming languages

define

commit

public beta

0

Followed

7

Example Questions

votes newest recent

Proof Assistants: What is the difference between “Locale” in Isabelle/HOL and dependent records in MLTT?

Proof Assistants: How do we Church-encode (or in any other lambda encoding styles) inductive-recursive types?

Proof Assistants: Why Agda's `--without-K` option also affects the indices of inductive types, where they have to be of smaller sizes?

Programming Language Design and Implementation: Since lazy-evaluation is, after the presence of Haskell, rarely used in popular languages, is it considered a bad feature now? For what reasons?

Proof Assistants: What common mistakes have people made in implementations of universe polymorphism and how are they addressed?

Programming Language Design and Implementation: What are the advantages of having first-class functions versus having only anonymous class with fancy sugars?

Programming Language Design and Implementation: Why do some programming languages choose to have a dedicated keyword for `elseif` instead of using `else` + `if` like in C?

16

Votes Cast

13 up

3 down

13

Badges

● Editor
● Nice Question × 4
● Filibuster

● Upholder
● Promoter
● Lobbyist

● Centrist
● Pioneer
● Advocate

● Autobiographer

user feed