NDLI: Algebras and coalgebras in the light affine Lambda calculus

Content Provider	ACM Digital Library
Author	Gaboardi, Marco Péchoux, Romain
Abstract	Algebra and coalgebra are widely used to model data types in functional programming languages and proof assistants. Their use permits to better structure the computations and also to enhance the expressivity of a language or of a proof system. Interestingly, parametric polymorphism à la System F provides a way to encode algebras and coalgebras in strongly normalizing languages without losing the good logical properties of the calculus. Even if these encodings are sometimes unsatisfying because they provide only limited forms of algebras and coalgebras, they give insights on the expressivity of System F in terms of functions that we can program in it. With the goal of contributing to a better understanding of the expressivity of Implicit Computational Complexity systems, we study the problem of defining algebras and coalgebras in the Light Affine Lambda Calculus, a system characterizing the complexity class FPTIME. This system limits the computational complexity of programs but it also limits the ways we can use parametric polymorphism, and in general the way we can write our programs. We show here that while the restrictions imposed by the Light Affine Lambda Calculus pose some issues to the standard System F encodings, they still permit to encode some form of algebra and coalgebra. Using the algebra encoding one can define in the Light Affine Lambda Calculus the traditional inductive types. Unfortunately, the corresponding coalgebra encoding permits only a very limited form of coinductive data types. To extend this class we study an extension of the Light Affine Lambda Calculus by distributive laws for the modality §. This extension has been discussed but not studied before.
Starting Page	114
Ending Page	126
Page Count	13
File Format	PDF
ISSN	03621340 15581160
DOI	10.1145/2858949.2784759
Journal	ACM SIGPLAN Notices (SIGP)
Volume Number	50
Issue Number	9
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	1983-05-01
Publisher Place	New York
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Algebra and coalgebra Light logics Implicit computational complexity
Content Type	Text
Resource Type	Article
Subject	Computer Graphics and Computer-Aided Design Software

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

Algebras and coalgebras in the light affine Lambda calculus

Algebras and Coalgebras in the Light Affine Lambda Calculus

Algebras and Coalgebras in the Light Affine Lambda Calculus

Light affine lambda calculus and polynomial time strong normalization

The Lambda Lambda-Bar calculus:a dual calculus for unconstrained strategies

Pure patterns type systems

Propositions as sessions

Functional back-ends within the lambda-sigma calculus

A Meta Lambda Calculus with Cross-Level Computation

Algebras and coalgebras in the light affine Lambda calculus

Similar Documents

Algebras and coalgebras in the light affine Lambda calculus

Algebras and Coalgebras in the Light Affine Lambda Calculus

Algebras and Coalgebras in the Light Affine Lambda Calculus

Light affine lambda calculus and polynomial time strong normalization

The Lambda Lambda-Bar calculus:a dual calculus for unconstrained strategies

Pure patterns type systems

Propositions as sessions

Functional back-ends within the lambda-sigma calculus

A Meta Lambda Calculus with Cross-Level Computation

Algebras and coalgebras in the light affine Lambda calculus