FGJ-omega in Coq

---

Library Util

• Useful Properties of Basic Datatypes

Library MatchCompNat

• Matching Integer Comparisons

Library WellFoundation

• Some Properties of Well-foundation

Library SimplyTypedLambdaCalculus

• Simply typed lambda-calculus

Library SimplyTypedLambdaCalculus_normalization

• Simply typed lambda-calculus (Strong normalization proof)

Library Syntax

• Definition of Syntax

Library Binders

• Representation of FGJ-omega binders using DeBruijn's indices

Library Substitutions

• Definition of Substitutions

Library Auxiliary

• Auxiliary definitions for FGJ-omega

Library Typing

• Definition of Typing in FGJ-omega

Library WellFormedness

• Definition of Well-formedness for Members, Classes and Programs

Library Semantics

• Definition of Semantics for FGJ-omega

Library Binders_proofs

• Representation of FGJ-omega binders using DeBruijn's indices (Proofs)

Library Substitutions_proofs

• Definition of Substitutions (Proofs)

Library Auxiliary_proofs

• Auxiliary definitions for FGJ-omega (Proofs)

Library Confluence

• Confluence of type reduction in FGJ-omega

Library Typing_proofs

• Definition of Typing in FGJ-omega (Proofs)

Library Subtyping_proofs

• Properties of subtyping in FGJ-omega (Proofs)

Library Normalization_proofs

• Proof of normalization of type reduction

Library TransitivityElimination_proofs

• Elimination of the transitivity rule

Library Progress_proofs

• Progress

Library BoundCompliantSubstitutions_proofs

• Proofs about substitutions that match bounds

Library TypeSubstitutionInTyping

• Type substitution in typing

Library TermSubstitutionInTyping

• Term substitution in typing

Library SubjectReduction_preliminaries

• Subject reduction (preliminaries)

Library SubjectReduction_proofs

• Subject reduction

Library TypeSafety

• Type safety

---

This page has been generated by coqdoc