MaiaVictor's user avatar
MaiaVictor's user avatar
MaiaVictor's user avatar
MaiaVictor
  • Member for 10 years, 8 months
  • Last seen more than a month ago
6 votes
4 answers
2k views

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

12 votes
3 answers
2k views

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

18 votes
1 answer
1k views

Can we derive Cubical Type Theory from Self-Types?

11 votes
1 answer
1k views

Are optimal evaluators actually optimal?

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
1k views

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

3 votes
2 answers
937 views

Is there a space efficient way to represent numbers on the lambda calculus?

10 votes
1 answer
920 views

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

2 votes
1 answer
734 views

Wouldn't the calculus of constructions with linear types be a simple functional core that is consistent and expressive?

1 vote
3 answers
633 views

Is there an array structure that allows for O(1) complexity for reverse, zip, slice etc operations?

4 votes
0 answers
522 views

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

6 votes
0 answers
461 views

How can unification be applied to interaction combinators?

12 votes
1 answer
459 views

An example where smallest normal lambda term is not fastest

5 votes
2 answers
451 views

Is there a "lambda cube" for interaction nets?

-2 votes
1 answer
437 views

What is the simplest known solver for a np-complete problem?

14 votes
0 answers
427 views

Are there simple core languages which are consistent and expressive?

10 votes
1 answer
416 views

Is `sort` typeable on elementary affine logic?

3 votes
0 answers
403 views

Is there any system where function equality (extensionality) is decidable?

3 votes
0 answers
389 views

Is it possible to check equality of equi-recursive types, or recursive λ-terms?

6 votes
1 answer
357 views

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

6 votes
2 answers
352 views

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

2 votes
3 answers
351 views

Is there any programming language in which any equivalent program has a unique, decidable normal representation?

12 votes
1 answer
347 views

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

5 votes
1 answer
338 views

Can a term on normal form prove an illogical assertion?

5 votes
3 answers
319 views

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

5 votes
1 answer
306 views

How can you encode natural numbers operations on interaction combinators?

6 votes
1 answer
299 views

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

4 votes
1 answer
299 views

What, in simple terms, are the restrictions imposed by Elementary Affine Logic?

2 votes
3 answers
298 views

Is there any language for which a perfect optimization is decidable?

0 votes
0 answers
295 views

Can $f^{2^N}(x)$ be computed in polynomial time when $f$ is linear?