Lifting Proof-Relevant Unification to Higher Dimensions

Jesper Cockx, Dominique Devriese

Research output: Chapter in Book/Report/Conference proceedingConference paper

1 Citation (Scopus)
Original languageEnglish
Title of host publicationProceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs
PublisherACM
Pages173-181
DOIs
Publication statusPublished - 2017
EventACM SIGPLAN Conference on Certified Programs and Proofs - Paris, France
Duration: 16 Jan 201717 Jan 2017
http://cpp2017.mpi-sws.org/

Conference

ConferenceACM SIGPLAN Conference on Certified Programs and Proofs
Abbreviated titleCPP
CountryFrance
CityParis
Period16/01/1717/01/17
Internet address

Keywords

  • Unification
  • Type Theory
  • Dependent Types
  • Inductive Families
  • Agda

Cite this