43 votes

Has anyone ever accidentally "proven" a false theorem with type-in-type?

I did this myself! (At least, if you interpret "incorrect" as "probably not true" rather than "demonstrably false".) In the early days of homotopy type theory, we were ...
Mike Shulman's user avatar
  • 3,040
40 votes
Accepted

Has anyone ever accidentally "proven" a false theorem with type-in-type?

Yes. In fact, there is a very interesting example which is tied to the history of dependent type theory: Per Martin-Löf, in his 1971 manuscript*, studied a system with type-in-type which famously ...
Loïc's user avatar
  • 1,459
29 votes
Accepted

What are the bases for different Proof Assistants?

There are a lot of bases, theories and techniques in proof assistants. Let me show you how deep the rabbit hole is (in suggested order of implementation): (Fibrational) Dependent Type Theories CoC (...
Namdak Tönpa's user avatar
27 votes

What are the bases for different Proof Assistants?

Here are some other points in the space: NuPrl has dependent types but is pretty different from, e.g., Coq; as I understand it, it's based on a model of untyped computation and proofs of well-...
Jason Gross's user avatar
  • 1,457
17 votes
Accepted

What are the motivations for different variants of categorical models of dependent type?

I would divide these models into three general groups. Structures that are more "categorical", arising naturally from categories "in nature" without the need for strictification ...
Mike Shulman's user avatar
  • 3,040
16 votes
Accepted

Easy ways to introduce inductive types

In principle, every indexed inductive type can be defined from $\bot$, $\top$, $\mathsf{Bool}$, $\Pi$, $\Sigma$, $\mathsf{W}$, $\mathsf{Id}$ and universes, with exactly the expected eliminators and ...
András Kovács's user avatar
15 votes

Bringing OOP features into proof assistants?

Object oriented programming cannot easily be integrated into proof assistants, because object types are naturally mixed-variance. For example, a Java interface like: ...
Neel Krishnaswami's user avatar
15 votes
Accepted

Bringing OOP features into proof assistants?

Semantics The main OOP investigation and modeling in second order type theory was done by Luca Cardelli and Martin Abadi, e.g. in Theory of Objects and later was continued by Anton Setzer in Object-...
Namdak Tönpa's user avatar
14 votes
Accepted

Can you build W-types out of natural numbers predicatively?

The answer is no. According to Anton Setzer's PhD thesis: Proof theoretical strength of Martin-Löf Type Theory with W-type and one universe: Aczel has shown in [Acz77] that Martin-Löf’s type theory ...
Couchy's user avatar
  • 2,211
13 votes

What are the bases for different Proof Assistants?

ACL2 is based on the logic of Common Lisp. This means several things: The universe (over which one quantifies and defines predicates) consists of the s-expressions. Logically, it is equivalent to ...
Couchy's user avatar
  • 2,211
11 votes
Accepted

What's the relationship between refinement types and dependent types?

Is there something that is only possible with refinement types, but not possible (or extremely hard to imitate) in dependent types? Yes. Refinement types make the notion of logical or ghost term ...
Neel Krishnaswami's user avatar
11 votes

What are the upsides and downsides of typed vs untyped conversion?

From the perspective of implementation of conversion checking, it really depends on the specific setting. For vanilla intuitionistic type theories without more exotic features (like cubical TT, ...
András Kovács's user avatar
10 votes
Accepted

Type Checking Undecidable in Extensional Type Theory

Extensional type theory is characterized by the reflection rule, which says that if the identity type ${\rm Id}(a,b)$ is inhabited, then $a\equiv b$ ($a$ and $b$ are judgmentally equal). It is called ...
Mike Shulman's user avatar
  • 3,040
8 votes

What's the relationship between refinement types and dependent types?

I am not sure that there is a unique definition of refinement types, but there is a common theme. In general, a system featuring refinement types is some kind of ML extended with a subset type ...
Pierre-Marie Pédrot's user avatar
8 votes

What about dependent types is useful for theorem provers?

A general-purpose proof assistant must be built on a foundation that is strong enough to represent most or all of mathematics, since proofs take place in mathematics. Dependent type theory, like ...
Mike Shulman's user avatar
  • 3,040
8 votes
Accepted

In the "Simply Easy!" paper, why is it safe to evaluate types in the empty environment?

All is well. The implementation distinguishes between bound variables, represented as Bound i where i :: Int and free variables, ...
Andrej Bauer's user avatar
  • 8,969
7 votes

What about dependent types is useful for theorem provers?

Dependent types allow quantifiers over values, which is very important in describing propositions. This is impossible in, for example, simple type theory (on the other hand, it is not necessary to ...
ice1000's user avatar
  • 6,124
7 votes
Accepted

What are the principal differences between Agda's core type theory and Coq's?

I will answer the headline question and ignore UTT (I believe thinking of Agda as UTT causes more confusion than it solves). There are very many differences between the theories Agda and Coq implement,...
James Wood's user avatar
6 votes

Are Logics Based on Dependent Types Stronger Than Ones Without?

Pretty much always, it means "this gadget is more annoying to formalise in HOL", not "this gadget is not possible to formalise in HOL." A simple example of this is formalising ...
Neel Krishnaswami's user avatar
6 votes
Accepted

How can you represent a dependent type visually?

I addressed some of these questions in my lecture “Spartan Type Theory” (PDF slides) at the UniMath 2017 school in Birmingham. In particular, slide 18 looks like this: Please look at the slides for ...
Andrej Bauer's user avatar
  • 8,969
6 votes

Universe inconsistency as an effect

I don't have an answer, but I would like to provide some buzzwords and references that will make it easier to find relevant literature. Some background information Computational effects and dependent ...
Andrej Bauer's user avatar
  • 8,969
6 votes

In a dependently typed language, are all types statements?

To make the basics clear: languages don't mean anything before you assign them meanings manually, and you can interpret the same language different ways. So if you want to interpret a dependent type ...
Trebor's user avatar
  • 3,867
5 votes

Formalization of abstract definitions

Maybe if you look at things the other way around, you’ll see why this is not a particularly deep feature from the type-theoretic point of view. Instead of viewing an abstracted definition as a ...
Meven Lennon-Bertrand's user avatar
5 votes
Accepted

How to implement first-order relational structures in Coq?

Supplemental: It looks like I misunderstood the point of the question and the OP might have simply been looking for the sig type, usually written as ...
Andrej Bauer's user avatar
  • 8,969
5 votes

What are the upsides and downsides of typed vs untyped conversion?

Typed conversion makes establishing metatheoretical properties of the syntax overwhelmingly easier, especially if you want to prove things like decidability of typechecking. Basically, when showing ...
Neel Krishnaswami's user avatar
5 votes
Accepted

Interpretation of dependent types: Coherence

I have commented with Curien's 1990 work on substitution up to isomorphisms, but you said it's too old. Here's a quite new reference, by Lumsdaine and Warren: https://arxiv.org/abs/1411.1736 It was ...
ice1000's user avatar
  • 6,124
5 votes

How to abstract over function arity in Lean and Coq?

I would like to focus on the following part of the question: I'd like to use such a construction to formalise universal algebra and apply the constructions and theorems of this theory to some ...
Andrej Bauer's user avatar
  • 8,969
5 votes
Accepted

What is a pattern in dependent pattern matching?

So there's a few things going on here. The picture you show is actually 3 different tables, placed side by side to preserve space. This is a sad effect of page limits for papers. The first column is ...
Joey Eremondi's user avatar
4 votes

Generic proof assistants/modularity of the proof assistants?

It sounds like you're after a logical framework, i.e., a system which allows you to reason within a given foundations. Isabelle is a bit more than this, it's a so-called "meta-logical framework&...
Alex Nelson's user avatar
  • 1,564
4 votes

What are the motivations for different variants of categorical models of dependent type?

I think they are here to show a particular thing of interest, because they're all very similar. There is always a category for contexts whose pullbacks correspond to substitutions, there's always a ...
ice1000's user avatar
  • 6,124

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