Damiano Mazza's user avatar
Damiano Mazza's user avatar
Damiano Mazza's user avatar
Damiano Mazza
  • Member for 10 years, 2 months
  • Last seen this week
25 votes
Accepted

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

22 votes

What is the contribution of lambda calculus to the field of theory of computation?

22 votes
Accepted

Can typed lambda calculi express *all* algorithms below a given complexity?

14 votes
Accepted

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

14 votes
Accepted

Do I have to give up the Law of the Excluded Middle in order to Learn $\lambda$-Calculus?

14 votes

(How) Could we discover/analyze NP problems in the absence of the Turing model of computation?

13 votes
Accepted

Contradiction between Gödel's Second Incompleteness Theorem and the Church-Rosser's property of CIC?

13 votes
Accepted

Can affine lambda calculus solve every problem in P?

13 votes
Accepted

Where is the model theory in programming language theory?

12 votes
Accepted

Is there an efficient beta-equivalence algorithm?

11 votes
Accepted

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

10 votes
Accepted

Why is the multi-step reduction of semantics reflexive?

10 votes
Accepted

Is there any known CCC closed under a probabilistic powerdomain operation?

10 votes

How does linear logic achieve resource management?

9 votes
Accepted

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

9 votes
Accepted

What is the complexity class of higher-order primitive recursion?

9 votes
Accepted

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

8 votes

How can you encode natural numbers operations on interaction combinators?

8 votes
Accepted

Do we care about confluence because of unique normal forms?

8 votes

Hierarchies in regular languages

8 votes
Accepted

What are the morphisms of Adj(C,T) - the category whose objects are the adjunctions of a given monad?

8 votes
Accepted

Are there strongly normalizing lambda terms that cannot be given a System F type?

7 votes
Accepted

A stronger multiplexing rule for soft linear logic?

7 votes
Accepted

Example of a term in system F which is not typable in the simply typed lambda calculus

7 votes
Accepted

In which posets is the set of compact elements downwards closed?

7 votes
Accepted

Difference between abstract machines and calculi

6 votes
Accepted

What is the relationship between intuitionistic logic, combinatory logic and lambda calculus?

6 votes
Accepted

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

6 votes
Accepted

Is length uniform AC0 computable?

6 votes
Accepted

Terminal object in the category of embeddings