# Questions tagged [typed-lambda-calculus]

The tag has no usage guidance.

36 questions
Filter by
Sorted by
Tagged with
3k views

### How do you get the Calculus of Constructions from the other points in the Lambda Cube?

The CoC is said to be the culmination of all three dimensions of the Lambda Cube. This isn't apparent to me at all. I think I understand the individual dimensions, and the combination of any two seems ...
1k views

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

I know that the complexity of most varieties of typed lambda calculi without the Y combinator primitive is bounded, i.e. only functions of bounded complexity can be expressed, with the bound becoming ...
1k views

### Is there a typed lambda calculus which is consistent and Turing complete?

Is there a typed lambda calculus where the corresponding logic under the Curry-Howard correspondence is consistent, and where there are typeable lambda expressions for every computable function? This ...
2k views

### Historic Relationship between Typed Lambda Calculus and Lisp?

I was having a discussion with a friend recently (who is an advocate of strongly typed languages). He made the comment: The inventors of Lambda Calculus always intended it to be typed. Now we can ...
171 views

### Eta expansion in the pattern lambda calculus

Klop, van Oostrom, and de Vrijer have a paper on the lambda calculus with patterns. http://www.sciencedirect.com/science/article/pii/S0304397508000571 In some sense, a pattern is a tree of variables ...
251 views

### Calculus of Constructions: compress expression to its smallest form

I'm aware that the Calculus of Constructions is strongly normalizing, meaning every expression has a normal for that cannot be beta,eta-reduced further. So in fact this is the most efficient ...
582 views

### Simply typed lambda calculus and higher order logic

What is the relation between simply typed lambda calculus and higher order logic? Under Curry-Howard it seems that simply typed lambda calculus corresponds to propositional logic. How is it related ...
445 views

### Proof techniques for showing that dependent type checking is decidable

I'm in a situation where I need to show that typechecking is decidable for a dependently-typed calculus I'm working on. So far, I've been able to prove that the system is strongly normalizing, and ...
193 views

### Program inversion algorithms for higher-order programs

The term program inversion has multiple shades of meaning, but probably got started with J. McCarthy's 1956 work The Inversion of Functions Defined by Turing Machines in the context of AI. By now ...
196 views

### Understanding the Proof of Strong Normalization of the Calculus of Constructions

I have difficulties in understanding the proof of strong normalization for the calculus of constructions. I try to follow the proof in the paper of Herman Geuvers "A short and flexible proof of Strong ...
172 views

### What's the difference between Moggi's computational metalanguage and Moggi's lambda calculus?

This is a reference confusion. Sometimes I see people use the term "Moggi's computational metalanguage" to refer to the calculus presented by Moggi, and sometimes to "Moggi's computational lambda ...
239 views

### Denotational semantics of System $F_\omega$ with recursive types and general recursion

Is there a denotational semantics for System $F_\omega$ in literature that supports both recursive types and general recursion? I'm looking for a model of Ralf Hinze's variant of System $F_\omega$ ...
191 views

### Termination checking for Scott-encodings in System F with positive-recursive types

Is there any research on termination analysis on Scott-encodings in System F with positive-recursive types. All papers I have found use languages with constructors and case analysis (for example ...
320 views

### Finding a common factor in $\lambda$-terms that agree under certain substitutions

Suppose that $\mathcal{L}$ is the language of a simply typed lambda calculus of two base types, $e$ and $t$, with infinitely many constants at each type. A substitution $j$ is a mapping from ...
166 views

### Structural equality of Pi Types with heterogeneous equality?

I'm trying to implement a proof of the following type: ...
241 views

### Fixed set of type constructors to simulate all intensional inductive families?

I'm wondering, are there small dependent calculi that can simulate a language with inductive families (that is, has a type isomorphic to each inductive family, at least as powerful of induction ...
211 views

217 views

### Moggi's computational metalanguage

In Notions of Computation and Monads Moggi models the notion of a computation of type $A$, $TA$, using a monad $T$. Among other things this ensures the $T\eta$ rule: \frac{x: A \vdash a:TB}{x:A \...
596 views

### Is simply typed lambda calculus equivalent to primitive recursive functions

It's well known that the computation models untyped lambda calculus and $\mu$-recursive function are equivalent in terms of computability (in fact they are both Turing complete.) It is also well known ...
154 views

### Heyting algebra in simply typed lambda calculus

The Emil Jeřábek's comment in Can boolean algebra be expressed in simply typed lambda caclulus? give rise to the following question: Can some non-trivial Heyting algebra be expressed in simply typed ...
We work in the Church-style simply typed lambda calculus. All terms shall be considered in long normal form. Any term of type $A_1\rightarrow A_2\ldots\rightarrow A_n \rightarrow 0$ is of the form \$\...