MaiaVictor's user avatar
MaiaVictor's user avatar
MaiaVictor's user avatar
MaiaVictor
  • Member for 10 years, 6 months
  • Last seen this week
17 votes
1 answer
1k views

Can we derive Cubical Type Theory from Self-Types?

14 votes
0 answers
425 views

Are there simple core languages which are consistent and expressive?

12 votes
1 answer
458 views

An example where smallest normal lambda term is not fastest

12 votes
3 answers
2k views

How to make the Lambda Calculus strong normalizing without a type system?

12 votes
1 answer
347 views

What makes a language (and its type-system) capable of proving theorems about its own terms?

11 votes
1 answer
1k views

Are optimal evaluators actually optimal?

10 votes
1 answer
415 views

Is `sort` typeable on elementary affine logic?

10 votes
1 answer
1k views

Can Elementary Affine Logic be used as the core type system of a practical programming language?

10 votes
1 answer
916 views

How do you encode Lamping's abstract algorithm using interaction combinators?

10 votes
1 answer
1k views

Algorithm to determine function equality on the simply typed lambda calculus?

7 votes
0 answers
225 views

Is there a programming language where any arbitrary recursive function can be fused?

7 votes
1 answer
238 views

Is it possible to unambiguously read back λ terms from interaction nets without node types?

7 votes
1 answer
240 views

If the untyped language is terminating, can we still derive a contradiction from `Type : Type`?

6 votes
1 answer
119 views

Can you assign a type to any term of the λEA-calculus?

6 votes
1 answer
154 views

Is CoC inconsistent with cnat_ind axiom?

6 votes
4 answers
2k views

How to introduce recursion to Simply Typed Lambda Calculus while at the same time keeping strong normalisation?

6 votes
2 answers
352 views

Is there an algorithm which gets incrementally "smarter" as it runs?

6 votes
1 answer
356 views

What type system fits the subclass of λ-terms that can be reduced optimally?

6 votes
1 answer
296 views

Can a totality checker be used to guarantee a proof on the calculus of constructions + inductive types is correct?

6 votes
0 answers
148 views

Is higher-order unification decidable for terms without abstractions within applications?

6 votes
0 answers
460 views

How can unification be applied to interaction combinators?

5 votes
1 answer
300 views

How can you encode natural numbers operations on interaction combinators?

5 votes
1 answer
105 views

Is it possible to evaluate interaction combinators efficiently using a path-traveling strategy?

5 votes
2 answers
441 views

Is there a "lambda cube" for interaction nets?

5 votes
3 answers
312 views

Is it possible to create a "quote" function that, given a native λ-term, returns its λ-encoded representation?

5 votes
1 answer
337 views

Can a term on normal form prove an illogical assertion?

4 votes
1 answer
157 views

Is there a simple algorithm for proof search on CoC?

4 votes
0 answers
236 views

Is my understanding regarding how to implement Quotient Types correct?

4 votes
0 answers
521 views

Is it possible to derive induction by extending CoC with recursion?

4 votes
1 answer
244 views

Why isn't it "enough" to prove induction with one extra "INat" argument?