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

[thumbnail of Ghani-etal-LNCS-2016-Proof-relevant-parametricity]
Preview
 Text (Ghani-etal-LNCS-2016-Proof-relevant-parametricity)
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 logoORCID: https://orcid.org/0000-0002-3988-2560, Nordvall Forsberg, Fredrik ORCID logoORCID: https://orcid.org/0000-0001-6157-9288 and Orsanigo, Federico; Lindley, Sam, McBride, Conor, Trinder, Phil and Sannella, Don
    • 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
      Keywords:computer science, computers, higher-dimensional, parametricity, polymorphic functions, relevant relations, type theory, artificial intelligence, Electronic computers. Computer science, Computer Science(all), Theoretical Computer Science
      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:17 Mar 2021 02:34
      Related URLs:
      URI:https://strathprints.strath.ac.uk/id/eprint/64286
    CORE (COnnecting REpositories)