Meaning explanations at higher dimension

Reference. Meaning explanations at higher dimension

Carlo Angiuli, Robert Harper · Indagationes Mathematicae · 2018 · cubical · DOI

Cite

Cite as @angiuli-2018-meaning (helia, typst) · \cite{angiuli-2018-meaning} (LaTeX)

BibTeX

bibtex · 1 line

@article{angiuli-2018-meaning, title={Meaning explanations at higher dimension}, volume={29}, ISSN={0019-3577}, url={http://dx.doi.org/10.1016/j.indag.2017.07.010}, DOI={10.1016/j.indag.2017.07.010}, number={1}, journal={Indagationes Mathematicae}, publisher={Elsevier BV}, author={Angiuli, Carlo and Harper, Robert}, year={2018}, month=Feb, pages={135–149} }

hayagriva YAML (typst)

yaml · 18 lines

angiuli-2018-meaning:
  type: article
  title: Meaning explanations at higher dimension
  author:
  - Angiuli, Carlo
  - Harper, Robert
  date: 2018-02
  page-range: 135-149
  url: http://dx.doi.org/10.1016/j.indag.2017.07.010
  serial-number:
    doi: 10.1016/j.indag.2017.07.010
    issn: 0019-3577
  parent:
    type: periodical
    title: Indagationes Mathematicae
    publisher: Elsevier BV
    issue: 1
    volume: 29

Download: angiuli-2018-meaning.bib · angiuli-2018-meaning.yml

Cited by (1)

First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory sterling_20212021

The implementation and semantics of dependent type theories can be studied in a syntax-independent way: the objective metatheory of dependent type theories exploits the universal properties of their syntactic categories to endow them with computational content, mathematical meaning, and practical implementation (normalization, type checking, elaboration). The semantic methods of the objective metatheory inform the design and implementation of correct-by-construction elaboration algorithms, promising a principled interface between real proof assistants and ideal mathematics. In this dissertation, I add synthetic Tait computability to the arsenal of the objective metatheorist. Synthetic Tait computability is a mathematical machine to reduce difficult problems of type theory and programming languages to trivial theorems of topos theory. First employed by Sterling and Harper to reconstruct the theory of program modules and their phase separated parametricity, synthetic Tait computability is deployed here to resolve the last major open question in the syntactic metatheory of cubical type theory: normalization of open terms.

DOI

Cites 51 works (3 here)

With notes (3)

Computational higher-dimensional type theory angiuli-2017-computationalPOPL · 2017

PDF · DOI · pldb

Homotopy Type Theory: Univalent Foundations of Mathematics hottbookarXiv · 2013

Web · arXiv

Observational equality, now! altenkirch-2007-observationalPLPV · 2007

DOI

External (48)

Cubical type theory: a constructive interpretation of the univalence axiom (2016)
On the Homotopy Groups of Spheres in Homotopy Type Theory (PhD thesis) (2016)
Practical Foundations for Programming Languages (2nd ed.) (2016)
Cubical Interpretations of Type Theory (PhD thesis) (2016)
The simplicial model of univalent foundations (after Voevodsky) (2016)
RedPRL - the People's Refinement Logic (2016)
The Coq proof assistant (2016)
The Lean theorem prover (system description) (2015)
Coq as a Metatheory for Nuprl with Bar Induction (2015)
A model of type theory in cubical sets (2014)
Quotient Types in Type Theory (PhD thesis) (2014)
A cubical type theory (Licata-Brunerie talk notes) (2014)
Quantum gauge field theory in cohesive homotopy type theory (2014)
The James construction and pi_4(S^3) (IAS talk video) (2013)
A Simple Type System with Two Identity Types (lecture notes) (2013)
Canonicity for 2-dimensional type theory (2012)
Types are weak ω-groupoids (2011)
Univalent foundations of mathematics (2011)
Homotopy type theory, VI (blog post) (2011)
The equivalence axiom and univalent models of type theory (talk notes) (2010)
UniMath: Univalent Mathematics (2010)
Homotopy theoretic models of identity types (2009)
Weak ω-categories from intensional type theory (2009)
The identity type weak factorisation system (2008)
Towards a Practical Programming Language Based on Dependent Type Theory (PhD thesis) (2007)
Identity types vs. weak omega-groupoids: some ideas, some problems (talk) (2006)
A very short note on homotopy lambda-calculus (2006)
Setoids in type theory (2003)
The groupoid interpretation of type theory (1998)
An operational approach to combining classical set theory and functional programming languages (1994)
Computational foundations of basic recursive function theory (1993)
Programming in Martin-Löf's Type Theory (1990)
Equality in lazy computation systems (1989)
Computational foundations of basic recursive function theory (LICS 1988) (1988)
Constructivism in Mathematics, Vol. I (1988)
A non-type-theoretic definition of Martin-Löf’s types (1987)
A Non-Type-Theoretic Semantics for Type-Theoretic Language (PhD thesis) (1987)
Implementing Mathematics with the Nuprl Proof Development System (1986)
Intuitionistic Type Theory (Bibliopolis) (1984)
Constructions, Proofs and the Meaning of Logical Constants (1983)
Constructive mathematics and computer programming (1982)
The formulae-as-types notion of construction (1980)
Elements of Intuitionism (1977)
An intuitionistic theory of types: predicative part (1975)
Metamathematical Investigation of Intuitionistic Arithmetic and Analysis (1973)
Foundations of Constructive Analysis (1967)
Abstract homotopy. I (1955)
Introduction to Metamathematics (1952)