Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

On the exp-log normal form of types

Danko Ilik 1
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : We present a type pseudo-normal form that any type built from arrows, products and sums can be isomorphically mapped to and that systematically minimizes the number of premises of sum type used. Inspired from a representation of exponential polynomials, the normal form presents an extension of the notion of disjunctive normal form that handles arrows. We also show how to apply it for simplifying the axioms of the theory of βη-equality of terms of the lambda calculus with sums.
Complete list of metadatas
Contributor : Danko Ilik <>
Submitted on : Tuesday, June 23, 2015 - 9:01:45 PM
Last modification on : Thursday, January 7, 2021 - 3:40:14 PM
Long-term archiving on: : Tuesday, September 15, 2015 - 10:26:21 PM


Files produced by the author(s)


  • HAL Id : hal-01167162, version 1


Danko Ilik. On the exp-log normal form of types. 2015. ⟨hal-01167162v1⟩



Record views


Files downloads