26 votes
Accepted

What was the original intent for the creation of Lambda calculus?

He wanted to create a formal system for the foundations of logic and mathematics that was simpler than Russell's type theory and Zermelo's set theory. The basic idea was to add a constant $\Xi$ to ...
24 votes
Accepted

Why was there a need for Martin-Löf to create intuitionistic type theory?

Very briefly: the simply-typed $\lambda$-calculus does not have dependent types. Dependent types were proposed by de Bruijn and Howard who wanted to extend the Curry-Howard correspondence from ...
21 votes
Accepted

Decidability of diophantine equations over {=, +, gcd}

($=$ is a logical symbol, hence I will not write it as part of the signature.) The satisfiability problem is decidable, as $\gcd$ has both a universal and an existential definition in terms of $|$, $+$...
20 votes
Accepted

Why do constructivists not seem to care too much about call/cc

Constructive mathematics is not just a formal system but rather an understanding of what mathematics is about. Or to put it differently, not every kind of semantics is accepted by a constructive ...
  • 26.8k
19 votes
Accepted

Do past time LTL and future time LTL have the same expressiveness?

The quick summary is that LTL with only past and no future modalities defines properties expressed over finite-words and these are the star-free subset of the regular languages. Standard LTL when ...
  • 12.4k
17 votes
Accepted

Why was Schönfinkel's work on eliminating "bound variables" in logic so crucial?

TL;DR. The metamathematics of binding are subtle: they seem trivial but aren't — whether you deal with (higher-order) logics or 𝜆-calculus. They're so subtle that binding representations form an open ...
  • 2,019
17 votes
Accepted

Entscheidungsproblem vs. Unvollständigkeitssatz (soft question)

The two words do not refer to the same thing. Hilbert's Entscheidungsproblem was the question whether there is an algorithm that decides the universal truth of first-order logical sentences, which was ...
15 votes

Are there any annotated formal verification systems for pure functional programming languages?

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 ...
  • 13.3k
15 votes
Accepted

Scott's stochastic lambda calculi

One apparent strength of his approach is that it allows higher-order functions (i.e. lambda terms) to be observable outcomes, which measure theory generally makes quite tricky. (The basic problem is ...
14 votes
Accepted

Logical Reations for an Impredicative System in a Predicative MetaTheory

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 ...
  • 13.3k
14 votes

Does the uncomputability of Kolmogorov complexity follow from Lawvere's Fixed Point Theorem?

EDIT: Adding the caveat that Roger's fixed-point theorem may not be a special case of Lawvere's. Here is a proof that may be "close"... It uses Roger's fixed-point theorem instead of Lawvere's ...
  • 8,316
13 votes
Accepted

Are there any annotated formal verification systems for pure functional programming languages?

Honda and Yoshida's A Compositional Program Logic for Polymorphic Higher-Order Functions (probably) pioneered Hoare logics for purely functional languages. This work is based on Hennessy-Milner ...
13 votes
Accepted

Ramification of An Impredicative Type Theory

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 ...
  • 13.3k
13 votes
Accepted

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

First, you are confusing consistency of CIC as an equational theory with consistency of CIC as a logical theory. The first means that not all terms of CIC (of the same type) are $\beta\eta$-equivalent....
13 votes
Accepted

Is there a good notion of non-termination and halting proofs in type theory?

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 ...
  • 13.3k
13 votes
Accepted

What logic correponds via Curry-Howard to a Monad?

The two papers to look at it are Benton, Bierman and de Paiva's Computational Types from a Logical Perspective, which directly gives a proof theory for Moggi's computational lambda-calculus; and Rowan ...
13 votes
Accepted

What is the complexity of checking equivalence of two boolean formulae without NOT symbol?

Note that formulas using $\land$ and $\lor$ gates (and possibly the constants $0$ and $1$) are known as monotone. The complexity of monotone formula equivalence depends on how complex formulas are ...
12 votes
Accepted

What is a term of the type $\bot\rightarrow A$?

There are several ways of writing such a term, depending on how we write the proof terms for the elimination rule for $\bot$, which is $$\frac{\quad\bot\quad}{A}$$ The corresponding rule in $\lambda$-...
  • 26.8k
12 votes
Accepted

Logical framework vs type theory

Summary. A logical framework is a meta-language for the formalisation of deductive systems, where deductions become syntactic objects. Of course what counts as a meta-language is quite vague, and it ...
12 votes

What is the difference between unification and anti-unification?

The following category theory inspired analysis (adapted from Plotkin's A Note on Inductive Generalization) explains a sense in which unification and anti-unification are dual concepts. As notation, ...
12 votes

Incomplete basis of combinators

[Expanding the comment into an answer.] First, just a clarification about counting bound variables in a combinator (= closed term) $t$. I interpret the question as asking about $$ \text{the total ...
12 votes
Accepted

Does the first order theory of a finite structure have bounded quantifier rank?

The theory of any finite structure is model complete. In fact, it is easy to see that any formula is equivalent to an existential formula with one quantifier per each element of the structure, after ...
12 votes

Why/when do we ever need transfinite loop variants?

You are correct when you observe that for any particular terminating loop $L$ we may simply define the invariant "we're getting one step closer to termination". But proving that this is indeed a valid ...
  • 26.8k
11 votes

Are there any annotated formal verification systems for pure functional programming languages?

See also Yann Régis-Gianas PhD thesis work with François Pottier: A Hoare Logic for Call-by-Value Functional Programs (MPC'08). This work was extended to cover the usual ML side-effects by Johannes ...
  • 1,910
11 votes
Accepted

Simply typed lambda calculus and higher order logic

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 ...
  • 13.3k
11 votes

Uses of $\infty$-categories in TCS

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 ...
  • 13.3k
11 votes

Uses of $\infty$-categories in TCS

Theoretical computer scientists do many things, one of which is mathematical modeling of various computer-sciency things. For instance, we like to provide mathematical models of programming languages, ...
  • 26.8k
11 votes
Accepted

Reference for the fact that (0=1) implies false requires a universe in MLTT

I know of: Jan M. Smith, The independence of Peano's fourth axiom from Martin-Löf's type theory without universes, The Journal of Symbolic Logic 53(3), p. 840-845, 1988.
11 votes
Accepted

Practical applications of parity games

Here is a rather different application from what you may have had in mind. Linear programming has many practical applications. There are many algorithms for linear programming and those based on ...
  • 12.4k
11 votes

Why do constructivists not seem to care too much about call/cc

As you note, there is a possible constructive interpretation of classical logic in this sense. The fact that classical logic is equiconsistent with intuitionistic logic (say, Heyting Arithmetic) has ...
  • 13.3k

Only top scored, non community-wiki answers of a minimum length are eligible