Search


Volume

Author

Year

  • < Previous
  • 1
  • Next >
5 results

Extended Initiality for Typed Abstract Syntax

Benedikt Ahrens.
Initial Semantics aims at interpreting the syntax associated to a signature as the initial object of some category of 'models', yielding induction and recursion principles for abstract syntax. Zsid\'o proves an initiality result for simply-typed syntax: given a signature S, the abstract syntax&nbsp;[&hellip;]
Published on April 6, 2012
Volume 8, Issue 2

Presentable signatures and initial semantics

Benedikt Ahrens ; André Hirschowitz ; Ambroise Lafont ; Marco Maggesi.
We present a device for specifying and reasoning about syntax for datatypes, programming languages, and logic calculi. More precisely, we study a notion of "signature" for specifying syntactic constructions. In the spirit of Initial Semantics, we define the "syntax generated by a signature" to be&nbsp;[&hellip;]
Published on May 26, 2021
Volume 17, Issue 2

Categorical structures for type theory in univalent foundations

Benedikt Ahrens ; Peter LeFanu Lumsdaine ; Vladimir Voevodsky.
In this paper, we analyze and compare three of the many algebraic structures that have been used for modeling dependent type theories: categories with families, split type-categories, and representable maps of presheaves. We study these in univalent type theory, where the comparisons between them&nbsp;[&hellip;]
Published on September 11, 2018
Volume 14, Issue 3

Displayed Categories

Benedikt Ahrens ; Peter LeFanu Lumsdaine.
We introduce and develop the notion of *displayed categories*. A displayed category over a category C is equivalent to "a category D and functor F : D --> C", but instead of having a single collection of "objects of D" with a map to the objects of C, the objects are given as a family indexed by&nbsp;[&hellip;]
Published on March 5, 2019
Volume 15, Issue 1

Initial Semantics for Reduction Rules

Benedikt Ahrens.
We give an algebraic characterization of the syntax and operational semantics of a class of simply-typed languages, such as the language PCF: we characterize simply-typed syntax with variable binding and equipped with reduction rules via a universal property, namely as the initial object of some&nbsp;[&hellip;]
Published on March 21, 2019
Volume 15, Issue 1
  • < Previous
  • 1
  • Next >