Share Your Experience: Take the 2024 Developer Survey

Tag Info

What should a proof of correctness for a typechecker actually be proving?

That's a good question! It asks what we expect from types in a typed language. First note that we can type any programing language with the unitype: just pick a letter, say ...
• 29.1k
Accepted

Yet another constructive (Coq) proof that nat -> nat -> nat is not bijective. How to explain it to myself?

First, let me say that "constructive" does not imply "all maps are Turing computable". It means “no excluded middle and axiom of choice were used“. In constructive mathematics the ...
• 29.1k
Accepted

Defining inductive types in intensional type theory purely in terms of type-theoretic data

It turns out that $W$ types plus identity types (eq/= in Coq) allow you to construct pretty much all the general inductive types ...

Formal semantics of OCaml in Coq

Have you seen Arthur Charguéraud's PhD thesis, Characteristic Formulae for Mechanized Program Verification? Rather than building the type system and small-step semantics as inductive relations, he ...
• 32.6k
Accepted

What should a proof of correctness for a typechecker actually be proving?

The question can be interpreted in two ways: Whether the implementation does implement a given typing system $T$? Whether the typing system $T$ does prevent the errors you think it should? The ...
• 11.5k
Accepted

What exactly is "large elimination"?

You are incorrect about the definition of large elimination: it refers to the ability to build values of type $\mathrm{Type}$ by eliminating an inductive value. The canonical example: ...
• 13.9k

Formal semantics of OCaml in Coq

You could be interested in Jacques Garrigue's A Certified Implementation of ML with Structural Polymorphism and Recursive Types, which establishes the soundness of static and dynamic semantics and ...
• 2,040
Accepted

• 1,629

Notation problem

You need to add a space after the d, before the ].

What exactly is "large elimination"?

Here is another attempt to illustrate large elimination. Consider the two following two ways to define a type: as an inductive or by induction. For instance, here are two definitions of a vector with ...
• 31

Modeling objects (OOP) in dependent type theory

There is a substantially expanded follow paper Andreas Abel, Stephan Adelsberger, Anton Setzer: Interactive Programming in Agda - Objects and Graphical User Interfaces. It contains an Agda library ...

Why does Coq have Prop?

The principle of propositions-as-types (or formulas-as-types), also known as the Curry-Howard correspondence, is the key idea for viewing (intuitionistic) type theories as logical systems and to apply ...

How does axiom K contradict univalence?

For a quick reference, here's (equation 8) a proof sketched in Agda. But I guess you're asking for the idea, and I think the reference is kinda technical. When you say 'univalence', you not only mean ...
• 965
1 vote
Accepted

Can I define nested mutually dependent types in Coq?

You can do mutually defined inductive types in Coq with the «with» syntax You end up with this definition: ...
• 26
1 vote

Yet another constructive (Coq) proof that nat -> nat -> nat is not bijective. How to explain it to myself?

To answer very directly: You have a constructive proof in Coq but it is not the case that the enum : nat -> nat is assumed (in Coq) to be computable. In a sense, ...
1 vote
Accepted

A Coq question : How to prove the image of the two same valued variables under a function are same?

You can't do that. You can actually define a function which doesn't respect Q's setoid structure. ...
1 vote

Defining functions on non-inductive types using LEM in Coq

I’m not sure I get what you are trying to do – or, rather, how your example corresponds to your goal. Indeed, in your code you postulate those three types a, ...
1 vote
Accepted

Lack of atomic propositions in the Calculus of Constructions from ATTAPL textbook

I have no thoughts on whether this is on-topic for TCS and if need be I can repost my answer elsewhere. But I think the question is a good opportunity to demonstrate how to think about the CoC pending ...
• 34

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