NDLI: The exp-log normal form of types: decomposing extensional equality and representing terms compactly

Please wait, while we are loading the content...

The influence of dependent types (keynote)

Ogre and Pythia: an invariance proof method for weak consistency models

Polymorphism, subtyping, and type inference in MLsub

Beginner's luck: a language for property-based generators

A promising semantics for relaxed-memory concurrency

Monadic second-order logic on finite sequences

A program optimization for automatic database result caching

Relational cost analysis

Deciding equivalence with sums and the empty type

Mixed-size concurrency: ARM, POWER, C/C++11, and SC

Type directed compilation of row-typed algebraic effects

A semantic account of metric preservation

Genesis: synthesizing forwarding tables in multi-tenant networks

Component-based synthesis for complex APIs

Intersection type calculi of bounded dimension

Parallel functional arrays

Big types in little runtime: open-world soundness and collaborative blame for gradual type systems

Invariants of quantum programs: characterisations and generation

LMS-Verify: abstraction without regret for verified systems programming

Rust: from POPL to practice (keynote)

A posteriori environment analysis with Pushdown Delta CFA

Java generics are turing complete

Exact Bayesian inference by symbolic disintegration

Automatically comparing memory consistency models

On the relationship between higher-order recursion schemes and higher-order fixpoint logic

Stream fusion, to completeness

Contract-based resource verification for higher-order functions with memoization

The exp-log normal form of types: decomposing extensional equality and representing terms compactly

Dynamic race detection for C++11

Cantor meets Scott: semantic foundations for probabilistic networks

LOIS: syntax and semantics

Learning nominal automata

Type soundness proofs with definitional interpreters

A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms

Gradual refinement types

The geometry of parallelism: classical, probabilistic, and quantum effects

Hypercollecting semantics and its application to static analysis of information flow

Semantic-directed clumping of disjunctive abstract states

Hazelnut: a bidirectionally typed structure editor calculus

Stochastic invariants for probabilistic termination

Interactive proofs in higher-order concurrent separation logic

Coming to terms with quantified reasoning

Rigorous floating-point mixed-precision tuning

Context-sensitive data-dependence analysis via linear conjunctive language reachability

Contextual isomorphisms

Serializability for eventual consistency: criterion, analysis, and applications

Dijkstra monads for free

On verifying causal consistency

Computational higher-dimensional type theory

Analyzing divergence in bisimulation semantics

Automatically generating the dynamic semantics of gradually typed languages

QWIRE: a core language for quantum circuits

LightDP: towards automating differential privacy proofs

Fast polyhedra abstract domain

Modules, abstraction, and parametric polymorphism

Coupling proofs are probabilistic product programs

A relational model of types-and-effects in higher-order concurrent separation logic

Towards automatic resource bound analysis for OCaml

Typed self-evaluation via intensional type functions

Thread modularity at many levels: a pearl in compositional verification

Stateful manifest contracts

Complexity verification using guided theorem enumeration

Type systems as macros

Fencing off go: liveness and safety for channel-based programming

Sums of uncertainty: refinements go gradual

The exp-log normal form of types: decomposing extensional equality and representing terms compactly

Content Provider	ACM Digital Library
Author	Ilik, Danko
Abstract	Lambda calculi with algebraic data types lie at the core of functional programming languages and proof assistants, but conceal at least two fundamental theoretical problems already in the presence of the simplest non-trivial data type, the sum type. First, we do not know of an explicit and implemented algorithm for deciding the beta-eta-equality of terms---and this in spite of the first decidability results proven two decades ago. Second, it is not clear how to decide when two types are essentially the same, i.e. isomorphic, in spite of the meta-theoretic results on decidability of the isomorphism. In this paper, we present the exp-log normal form of types---derived from the representation of exponential polynomials via the unary exponential and logarithmic functions---that any type built from arrows, products, and sums, can be isomorphically mapped to. The type normal form can be used as a simple heuristic for deciding type isomorphism, thanks to the fact that it is a systematic application of the high-school identities. We then show that the type normal form allows to reduce the standard beta-eta equational theory of the lambda calculus to a specialized version of itself, while preserving completeness of the equality on terms. We end by describing an alternative representation of normal terms of the lambda calculus with sums, together with a Coq-implemented converter into/from our new term calculus. The difference with the only other previously implemented heuristic for deciding interesting instances of eta-equality by Balat, Di Cosmo, and Fiore, is that we exploits the type information of terms substantially and this often allows us to obtain a canonical representation of terms without performing a sophisticated term analyses. .
Starting Page	387
Ending Page	399
Page Count	13
File Format	PDF
ISBN	9781450346603
DOI	10.1145/3009837.3009841
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2017-01-01
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Normal type Eta equality Normal term Type isomorphism Sum type Type-directed partial evaluation
Content Type	Text
Resource Type	Article

Central Library (ISO-9001:2015 Certified)
Indian Institute of Technology Kharagpur
Kharagpur, West Bengal, India | PIN - 721302

See location in the Map
03222 282435
Mail: support@ndl.gov.in

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in