cody
  • Member for 10 years, 11 months
  • Last seen this week
What functions can System F not compute?
Accepted answer
50 votes

System $F$ is quite expressive. As proved by Girard here, the functions of type $\mathbb{N}\rightarrow\mathbb{N}$ (where $\mathbb{N}$ is defined to be $\forall X.\ X\rightarrow (X\rightarrow X)\...

View answer
How to find interesting research problems
Accepted answer
40 votes

I strongly disagree with the "find a list of open problems" approach. Usually open problems are quite hard to make progress on, and I'm thoroughly unconvinced that good research is done by tackling ...

View answer
Algebra oriented branch of theoretical computer science
27 votes

There have been recent developments in dependent type theory which relate type systems to homotopy types. This is now a relatively small field, but there is a lot of exciting work being done right ...

View answer
What's the relation and difference between Calculus of Inductive Constructions and Intuitionistic Type Theory?
25 votes

I've already answered somewhat, but I'll try to give a more detailed overview of the type theoretical horizon, if you will. I'm a bit fuzzy on the historical specifics, so more informed readers will ...

View answer
To what extent can an algorithm predict the time complexity an arbitrary input program?
Accepted answer
23 votes

In general you cannot determine complexity, even for halting programs: let $T$ be some arbitrary Turing machine and let $p_T$ be the program (that always returns 0): input: n run T for n steps if T ...

View answer
How do you get the Calculus of Constructions from the other points in the Lambda Cube?
22 votes

I've often wanted to try and summarize each dimension of the $\lambda$-cube and what they represent, so I'll give this one a shot. But first, one should probably try to dis-entangle various issues. ...

View answer
Why does Coq have Prop?
22 votes

$\mathrm{Prop}$ is impredicative, which create a very expressive proof system. However it is "too" expressive in the following sense: $$ \mathrm{impredicative\ Prop} + \mathrm{large\ elimination} + \...

View answer
Is there a typed lambda calculus which is consistent and Turing complete?
21 votes

Alright I'll give a crack at it: In general for a given type system $T$, the following is true: If all well-type terms in the calculus $T$ are normalizing, then $T$ is consistent when viewed as a ...

View answer
Is MLTT effectively pCiC without Prop?
Accepted answer
20 votes

The short answer is yes, MLTT can reasonably be equated with CIC without impredicative Prop. The main technical issue is that there are dozens of variants when one talks about Martin-Löf Type Theory ...

View answer
Relative consistency of PA and some type theories
Accepted answer
20 votes

The short answer to your question 1 is no, but for perhaps subtle reasons. First of all, System $F$ and $F_\omega$ cannot express the first-order theory of arithmetic, and even less the consistency ...

View answer
How is Lambda Calculus a specific type of Term Writing system?
Accepted answer
17 votes

The answer is it depends what you mean by Term Rewrite System. When it was introduced, the concept of Term Rewrite Systems, or TRSes, described what is now called first order TRSes, which is simply a ...

View answer
Author ordering in TCS papers
16 votes

A quick bit of googling gives this for the RSA paper: Rivest stayed up all night, preparing the manuscript describing the code before he handed it to Adleman. He had listed the paper's authors in ...

View answer
Are there any annotated formal verification systems for pure functional programming languages?
15 votes

You might want to check out Liquid Haskell, which allow working with type refinements rather than dependent types. Type refinements can be seen as a restricted logical language that allow you to ...

View answer
Logical Reations for an Impredicative System in a Predicative MetaTheory
Accepted answer
14 votes

In general, what we usually call the logical relations argument isn't really linked to impredicativity: the main idea is simply to interpret terms in some abstract algebra $\cal A$, and to represent ...

View answer
Implementation of alpha equivalence
14 votes

The author is not misinformed, I'm afraid; it's part of the development process of any computer scientist to go through several phases: Phase 1: $\alpha$-equivalence is easy! Why is everyone making a ...

View answer
Is there a good notion of non-termination and halting proofs in type theory?
Accepted answer
13 votes

Because one of the principal applications of Type Theory in formalizations has been to study programing languages and computation in general, a lot of thought has gone into ways of representing ...

View answer
Ramification of An Impredicative Type Theory
Accepted answer
13 votes

I'm going to elaborate my comments into an answer. The origins of predicative type theory are almost as old as type theory itself, since one of Russel's motivations was to ban "circular" definitions ...

View answer
Is compiler for dependent type much harder than an intepreter?
Accepted answer
13 votes

This is an interesting question! As Anthony's answer suggests, one can use the usual approaches to compiling a non-dependent functional language, provided you already have an interpreter to evaluate ...

View answer
Is there an expressiveness hierarchy for type systems?
13 votes

I'm not sure I have a satisfactory answer to your question, but if you consider Pure Type Systems, which are a generalization of the systems found in the lambda cube (a thorough, if somewhat dated ...

View answer
funsplit and polarity of Pi-types
Accepted answer
12 votes

The presentation of functional elimination using $\mathrm{funsplit}$ is most definitely not a usual occurrence in most treatments of type theory. However, I believe that this form is indeed the "...

View answer
Has a proof checker bug ever invalidated a major proof?
Accepted answer
11 votes

To my knowledge, no machine checked proof of a complex mathematical development has ever been retracted. As Andrej points out though, it occasionally happens that soundness-breaking bugs do crop up ...

View answer
Typo in the calculus of constructions paper?
Accepted answer
11 votes

You are correct, there is an error in that paper, and the rule should indeed read: $$\frac{\Gamma\vdash M:\Delta}{\Gamma\vdash M\cong M} $$ the use of jugements of this style for equality (sometimes ...

View answer
What's the relation between OOP and category theory?
11 votes

There are absolutely some relationships between the semantics and practice of OOP and category theory. This is somewhat unsurprising since both fields attempt to give a principled generic account of ...

View answer
Uses of $\infty$-categories in TCS
11 votes

Applying higher homotopy-theoretic ideas to CS is still a very nascent field! My understanding is that it's not even that old as a mathematical field. Certainly HoTT is the central impetus for such ...

View answer
Simply typed lambda calculus and higher order logic
Accepted answer
11 votes

The distinction is this: if STLC is taken as a primitive language at the type-level adding constructors and a small number of axioms is sufficient to give you the full expressive power of HOL. Taking ...

View answer
What are some good introductory books on type theory?
11 votes

Barendregts Lambda Calculi with Types is more advanced, but it covers some important topics in the "classical" theory of types.

View answer
Is it possible to decide $\beta$-equivalence within System F (or another normalizing typed λ-calculus)?
11 votes

Another possible answer to Neel's perfectly correct one: Suppose that there is a combinator $E$, well-typed in system F such that the above condition holds. The type of $E$ is: $$ E : \forall \alpha.\...

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

I'm going to assume that by $\mathrm{Fix}$ you mean a new type constructor $$\frac{\Gamma\vdash F:*\rightarrow *}{\Gamma\vdash \mathrm{Fix}\ F:*} $$ Along with the conversion rule $\mathrm{Fix}\ F\...

View answer
Decidability of type inference and type checking in MLTT
Accepted answer
10 votes

Certainly the decision problem Given a (pre-)term $a$ Is there a type $A$ such that $\vdash a :A$ is derivable in MLTT? Sometimes written $\vdash a\ :\ ?$ (and called the type inference problem) ...

View answer
Church-Rosser property for dependently typed lambda calculus?
Accepted answer
10 votes

It might be useful to quickly give the counter-example to CR in typed calculi with $\beta$ and $\eta$: $$ t=\lambda x:A.(\lambda y:B.\ y)\ x$$ And we have $$ t\rightarrow_\beta \lambda x: A.x$$ and $...

View answer
1
2 3 4 5 6