• Home
• About Coq
• Get Coq
• Documentation
• Community

Library PTSATR.ut_typ_eq_inj

• Definition of a weaker form a Pi injectivity for PTSe

Library PTSATR.counter_ex

• Counter Example for Strong Pi injectivity in PTSe.

Library PTSATR.final_result

• Final Result : PTS <-> PTSe

Library PTSATR.glue

• Validity of Annotations

Library PTSATR.typ_annot

• Definition of PTS{atr} and proof of Confluence

Library PTSATR.strip

• Stripping functions

Library PTSATR.red

• Beta reduction for annotated terms

Library PTSATR.env

• Typing Environment for annotated terms .

Library PTSATR.term

• Annotated Terms syntax

Library PTSATR.ut_strengh

• Strenghthening

Library PTSATR.ut_typ_eq

• Definition of PTS with Judgmental Equality (PTSe)
• Type Correctness
• Left-Hand Reflexivity
• Right-Hand Reflexivity

Library PTSATR.ut_sr

• The Subject Reduction Property.

Library PTSATR.ut_typ

Library PTSATR.ut_red

• Beta-reduction definition and properties.
  • Usual Beta-reduction:
  • Parallel Reduction

Library PTSATR.ut_env

• Typing Environment Definition and Function Manipulation.

Library PTSATR.ut_term

• Term definition for PTS and de Bruijn manipulation .
• Usual Term syntax .

Library PTSATR.base

• Abstract Parameters of PTS
  • Sorts and Variables

• webmaster
• xhtml valid
• CSS valid