Area 51 » ice1000

info activity reputation

reputation

59 views

discussion user

network profile

Registered User

name	ice1000
member for	2 years
seen	May 18 at 22:09
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

662

days

Proof Assistants

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

define

commit

public beta

200

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?

8

Votes Cast

7 up

1 down

12

Badges

● Nice Question × 4
● Filibuster

● Upholder
● Promoter

● Lobbyist
● Centrist

● Pioneer
● Advocate

● Autobiographer

user feed