Proof-relevant parametricity

Ghani, Neil and Nordvall Forsberg, Fredrik and Orsanigo, Federico; Lindley, Sam and McBride, Conor and Trinder, Phil and Sannella, Don, eds. (2016) Proof-relevant parametricity. In: A List of Successes That Can Change the World. Lecture Notes in Computer Science . Springer-Verlag, Switzerland, pp. 109-131. ISBN 9783319309354 (https://doi.org/10.1007/978-3-319-30936-1_6)

Preview

Text. Filename: Ghani_etal_LNCS_2016_Proof_relevant_parametricity.pdf Accepted Author Manuscript Download (461kB)| Preview

Abstract

Parametricity is one of the foundational principles which underpin our understanding of modern programming languages. Roughly speaking, parametricity expresses the hidden invariants that programs satisfy by formalising the intuition that programs map related inputs to related outputs. Traditionally parametricity is formulated with proofirrelevant relations but programming in Type Theory requires an extension to proof-relevant relations. But then one might ask: can our proofs that polymorphic functions are parametric be parametric themselves? This paper shows how this can be done and, excitingly, our answer requires a trip into the world of higher dimensional parametricity.

ORCID iDs

Ghani, Neil ORCID: https://orcid.org/0000-0002-3988-2560

Nordvall Forsberg, Fredrik ORCID: https://orcid.org/0000-0001-6157-9288

• Share and Export
  

  RDF+XMLBibTeXRIOXX2 XMLRDF+N-TriplesJSONDublin CoreAtomSimple MetadataReferMETSHTML CitationASCII CitationOpenURL ContextObjectEndNoteOpenURL ContextObject in SpanMODSMPEG-21 DIDLEP3 XMLData Cite XMLRIS (EndNote Online, Zotero, Ref manager, etc)RDF+N3Multiline CSV
• Item metadata

  Item type:	Book Section
  ID code:	64286
  Dates:	Date Event 25 March 2016 Published 5 December 2015 Accepted
  Notes:	This is a post-peer-review, pre-copyedit version of an article published in Lecture Notes in Computer Science. The final authenticated version is available online at: https://doi.org/10.1007/978-3-319-30936-1_6
  Subjects:	Science > Mathematics > Electronic computers. Computer science
  Department:	Faculty of Science > Computer and Information Sciences
  Depositing user:	Pure Administrator
  Date deposited:	06 Jun 2018 15:31
  Last modified:	11 Nov 2024 15:05
  Related URLs:	Scopus publication
  URI:	https://strathprints.strath.ac.uk/id/eprint/64286