Damiano Mazza's user avatar
Damiano Mazza's user avatar
Damiano Mazza's user avatar
Damiano Mazza
  • Member for 9 years, 11 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?

12 votes
Accepted

Is there an efficient beta-equivalence algorithm?

12 votes
Accepted

Where is the model theory in programming language theory?

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

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

How do conference proceedings add to academic prestige?

6 votes

Calculus of Constructions: compress expression to its smallest form