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 ...
• 26.8k
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 ...
• 31.8k
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 ...
• 10.4k
Accepted

Examples of Universe inconsistency in normal use of dependent types

This is a hard question to answer, in part because it's unclear what it means to get something "by accident". Regularly, though, people run into the ...
• 13.3k
Accepted

• 1,349

• 4,319

How would I go about learning the underlying theory of the Coq proof assistant?

The current Software Foundations book does explain all this later on: https://softwarefoundations.cis.upenn.edu/lf-current/ProofObjects.html So if you're following the book, just read on :)

Featherweight Generic Java formalization in Coq

I guess somewhat more realistic task would be to find Coq's formalisation of FJ itself (probably with some extensions, but not necessarily FGJ). The one which I googled easily is: Encoding ...
• 1,083

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 ...

Law of excluded middle in MLTT

Adding LEM to MLTT is no problem. You simply need to assume a term of type forall P:Prop, P \/ ~ P. In Coq, you can use the LEM as follows: ...

Is there an algorithm to generate proof in Coq?

I guess the resource you are looking for is Adam Chlipala's Certified Programming with Dependent Types in which he builds up powerful tactics.
• 636

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 ...
• 923
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