Area 51 » ice1000

info activity reputation

429

reputation

41 views

discussion user

network profile

Registered User

name	ice1000
member for	1 year
seen	Mar 19 at 22:33
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

Proposals

Current Commitment

163

committed

Programming Language Design and Implementation

For designers and implementers of computer programming languages

define

commit

beta

Fulfilled Commitment

415

days

Proof Assistants

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

define

commit

public beta

Followed

163

committed

Programming Language Design and Implementation

For designers and implementers of computer programming languages

define

commit

beta

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?

Votes Cast

7 up

1 down

Badges

● Nice Question × 4
● Filibuster

● Upholder
● Promoter

● Lobbyist
● Centrist

● Pioneer
● Advocate

● Autobiographer

user feed