Simply typed lambda calculus with opposite types

ABSTRACT: In this article we present an extension of simply typed lambda calculus by introducing the idea of opposite types developed by Agudelo-Agudelo and Sicard-Ramírez (2021). The rules for these new types are based on the rules of a fragment of the logic system presented by the same authors. Tw...

Full description

Autores:
Pinilla Barrera, Alejandro
Tipo de recurso:
Trabajo de grado de pregrado
Fecha de publicación:
2022
Institución:
Universidad de Antioquia
Repositorio:
Repositorio UdeA
Idioma:
eng
OAI Identifier:
oai:bibliotecadigital.udea.edu.co:10495/27314
Acceso en línea:
http://hdl.handle.net/10495/27314
Palabra clave:
Lambda calculus
Type theory
Curry-Howard isomorphism
Logic, symbolic and mathematical
Lógica simbólica y matemática
Tipos opuestos
Normalización fuerte
http://id.loc.gov/authorities/subjects/sh85074174
http://id.loc.gov/authorities/subjects/sh85139126
http://id.loc.gov/authorities/subjects/sh2001002954
http://id.loc.gov/authorities/subjects/sh85078115
Rights
openAccess
License
Atribución-NoComercial-CompartirIgual 2.5 Colombia (CC BY-NC-SA 2.5 CO)
id UDEA2_415cf7956b67786a7d0287d0e0ff2b45
oai_identifier_str oai:bibliotecadigital.udea.edu.co:10495/27314
network_acronym_str UDEA2
network_name_str Repositorio UdeA
repository_id_str
dc.title.spa.fl_str_mv Simply typed lambda calculus with opposite types
title Simply typed lambda calculus with opposite types
spellingShingle Simply typed lambda calculus with opposite types
Lambda calculus
Type theory
Curry-Howard isomorphism
Logic, symbolic and mathematical
Lógica simbólica y matemática
Tipos opuestos
Normalización fuerte
http://id.loc.gov/authorities/subjects/sh85074174
http://id.loc.gov/authorities/subjects/sh85139126
http://id.loc.gov/authorities/subjects/sh2001002954
http://id.loc.gov/authorities/subjects/sh85078115
title_short Simply typed lambda calculus with opposite types
title_full Simply typed lambda calculus with opposite types
title_fullStr Simply typed lambda calculus with opposite types
title_full_unstemmed Simply typed lambda calculus with opposite types
title_sort Simply typed lambda calculus with opposite types
dc.creator.fl_str_mv Pinilla Barrera, Alejandro
dc.contributor.advisor.none.fl_str_mv Agudelo Agudelo, Juan Carlos
Sicard Ramírez, Andrés
dc.contributor.author.none.fl_str_mv Pinilla Barrera, Alejandro
dc.subject.lcsh.none.fl_str_mv Lambda calculus
Type theory
Curry-Howard isomorphism
Logic, symbolic and mathematical
topic Lambda calculus
Type theory
Curry-Howard isomorphism
Logic, symbolic and mathematical
Lógica simbólica y matemática
Tipos opuestos
Normalización fuerte
http://id.loc.gov/authorities/subjects/sh85074174
http://id.loc.gov/authorities/subjects/sh85139126
http://id.loc.gov/authorities/subjects/sh2001002954
http://id.loc.gov/authorities/subjects/sh85078115
dc.subject.lemb.none.fl_str_mv Lógica simbólica y matemática
dc.subject.proposal.spa.fl_str_mv Tipos opuestos
Normalización fuerte
dc.subject.lcshuri.none.fl_str_mv http://id.loc.gov/authorities/subjects/sh85074174
http://id.loc.gov/authorities/subjects/sh85139126
http://id.loc.gov/authorities/subjects/sh2001002954
http://id.loc.gov/authorities/subjects/sh85078115
description ABSTRACT: In this article we present an extension of simply typed lambda calculus by introducing the idea of opposite types developed by Agudelo-Agudelo and Sicard-Ramírez (2021). The rules for these new types are based on the rules of a fragment of the logic system presented by the same authors. Two of the main properties of type systems are proven: The strong normalization theorem and the Curry-Howard correspondence.
publishDate 2022
dc.date.accessioned.none.fl_str_mv 2022-04-05T16:26:23Z
dc.date.available.none.fl_str_mv 2022-04-05T16:26:23Z
dc.date.issued.none.fl_str_mv 2022
dc.type.spa.fl_str_mv info:eu-repo/semantics/bachelorThesis
dc.type.coarversion.fl_str_mv http://purl.org/coar/version/c_b1a7d7d4d402bcce
dc.type.hasversion.spa.fl_str_mv info:eu-repo/semantics/draft
dc.type.coar.spa.fl_str_mv http://purl.org/coar/resource_type/c_7a1f
dc.type.redcol.spa.fl_str_mv https://purl.org/redcol/resource_type/TP
dc.type.local.spa.fl_str_mv Tesis/Trabajo de grado - Monografía - Pregrado
format http://purl.org/coar/resource_type/c_7a1f
status_str draft
dc.identifier.uri.none.fl_str_mv http://hdl.handle.net/10495/27314
url http://hdl.handle.net/10495/27314
dc.language.iso.spa.fl_str_mv eng
language eng
dc.rights.spa.fl_str_mv info:eu-repo/semantics/openAccess
dc.rights.*.fl_str_mv Atribución-NoComercial-CompartirIgual 2.5 Colombia (CC BY-NC-SA 2.5 CO)
dc.rights.uri.*.fl_str_mv http://creativecommons.org/licenses/by-nc-nd/2.5/co/
dc.rights.accessrights.spa.fl_str_mv http://purl.org/coar/access_right/c_abf2
dc.rights.creativecommons.spa.fl_str_mv https://creativecommons.org/licenses/by-nc-sa/4.0/
eu_rights_str_mv openAccess
rights_invalid_str_mv Atribución-NoComercial-CompartirIgual 2.5 Colombia (CC BY-NC-SA 2.5 CO)
http://creativecommons.org/licenses/by-nc-nd/2.5/co/
http://purl.org/coar/access_right/c_abf2
https://creativecommons.org/licenses/by-nc-sa/4.0/
dc.format.extent.spa.fl_str_mv 32
dc.format.mimetype.spa.fl_str_mv application/pdf
dc.publisher.place.spa.fl_str_mv Medellín, Colombia
institution Universidad de Antioquia
bitstream.url.fl_str_mv https://bibliotecadigital.udea.edu.co/bitstream/10495/27314/1/PinillaAlejandro_2022_SimplyTypedLambda.pdf
https://bibliotecadigital.udea.edu.co/bitstream/10495/27314/2/license_rdf
https://bibliotecadigital.udea.edu.co/bitstream/10495/27314/3/license.txt
bitstream.checksum.fl_str_mv 472dde3aa854eae752525ac5f7fffe78
b88b088d9957e670ce3b3fbe2eedbc13
8a4605be74aa9ea9d79846c1fba20a33
bitstream.checksumAlgorithm.fl_str_mv MD5
MD5
MD5
repository.name.fl_str_mv Repositorio Institucional Universidad de Antioquia
repository.mail.fl_str_mv andres.perez@udea.edu.co
_version_ 1812173303778902016
spelling Agudelo Agudelo, Juan CarlosSicard Ramírez, AndrésPinilla Barrera, Alejandro2022-04-05T16:26:23Z2022-04-05T16:26:23Z2022http://hdl.handle.net/10495/27314ABSTRACT: In this article we present an extension of simply typed lambda calculus by introducing the idea of opposite types developed by Agudelo-Agudelo and Sicard-Ramírez (2021). The rules for these new types are based on the rules of a fragment of the logic system presented by the same authors. Two of the main properties of type systems are proven: The strong normalization theorem and the Curry-Howard correspondence.32application/pdfenginfo:eu-repo/semantics/draftinfo:eu-repo/semantics/bachelorThesishttp://purl.org/coar/resource_type/c_7a1fhttps://purl.org/redcol/resource_type/TPTesis/Trabajo de grado - Monografía - Pregradohttp://purl.org/coar/version/c_b1a7d7d4d402bcceinfo:eu-repo/semantics/openAccessAtribución-NoComercial-CompartirIgual 2.5 Colombia (CC BY-NC-SA 2.5 CO)http://creativecommons.org/licenses/by-nc-nd/2.5/co/http://purl.org/coar/access_right/c_abf2https://creativecommons.org/licenses/by-nc-sa/4.0/Lambda calculusType theoryCurry-Howard isomorphismLogic, symbolic and mathematicalLógica simbólica y matemáticaTipos opuestosNormalización fuertehttp://id.loc.gov/authorities/subjects/sh85074174http://id.loc.gov/authorities/subjects/sh85139126http://id.loc.gov/authorities/subjects/sh2001002954http://id.loc.gov/authorities/subjects/sh85078115Simply typed lambda calculus with opposite typesMedellín, ColombiaMatemáticoPregradoFacultad de Ciencias Exactas y Naturales. MatemáticasUniversidad de AntioquiaORIGINALPinillaAlejandro_2022_SimplyTypedLambda.pdfPinillaAlejandro_2022_SimplyTypedLambda.pdfTrabajo de grado de pregradoapplication/pdf420153https://bibliotecadigital.udea.edu.co/bitstream/10495/27314/1/PinillaAlejandro_2022_SimplyTypedLambda.pdf472dde3aa854eae752525ac5f7fffe78MD51CC-LICENSElicense_rdflicense_rdfapplication/rdf+xml; charset=utf-8823https://bibliotecadigital.udea.edu.co/bitstream/10495/27314/2/license_rdfb88b088d9957e670ce3b3fbe2eedbc13MD52LICENSElicense.txtlicense.txttext/plain; charset=utf-81748https://bibliotecadigital.udea.edu.co/bitstream/10495/27314/3/license.txt8a4605be74aa9ea9d79846c1fba20a33MD5310495/27314oai:bibliotecadigital.udea.edu.co:10495/273142022-04-05 11:28:49.846Repositorio Institucional Universidad de Antioquiaandres.perez@udea.edu.coTk9URTogUExBQ0UgWU9VUiBPV04gTElDRU5TRSBIRVJFClRoaXMgc2FtcGxlIGxpY2Vuc2UgaXMgcHJvdmlkZWQgZm9yIGluZm9ybWF0aW9uYWwgcHVycG9zZXMgb25seS4KCk5PTi1FWENMVVNJVkUgRElTVFJJQlVUSU9OIExJQ0VOU0UKCkJ5IHNpZ25pbmcgYW5kIHN1Ym1pdHRpbmcgdGhpcyBsaWNlbnNlLCB5b3UgKHRoZSBhdXRob3Iocykgb3IgY29weXJpZ2h0Cm93bmVyKSBncmFudHMgdG8gRFNwYWNlIFVuaXZlcnNpdHkgKERTVSkgdGhlIG5vbi1leGNsdXNpdmUgcmlnaHQgdG8gcmVwcm9kdWNlLAp0cmFuc2xhdGUgKGFzIGRlZmluZWQgYmVsb3cpLCBhbmQvb3IgZGlzdHJpYnV0ZSB5b3VyIHN1Ym1pc3Npb24gKGluY2x1ZGluZwp0aGUgYWJzdHJhY3QpIHdvcmxkd2lkZSBpbiBwcmludCBhbmQgZWxlY3Ryb25pYyBmb3JtYXQgYW5kIGluIGFueSBtZWRpdW0sCmluY2x1ZGluZyBidXQgbm90IGxpbWl0ZWQgdG8gYXVkaW8gb3IgdmlkZW8uCgpZb3UgYWdyZWUgdGhhdCBEU1UgbWF5LCB3aXRob3V0IGNoYW5naW5nIHRoZSBjb250ZW50LCB0cmFuc2xhdGUgdGhlCnN1Ym1pc3Npb24gdG8gYW55IG1lZGl1bSBvciBmb3JtYXQgZm9yIHRoZSBwdXJwb3NlIG9mIHByZXNlcnZhdGlvbi4KCllvdSBhbHNvIGFncmVlIHRoYXQgRFNVIG1heSBrZWVwIG1vcmUgdGhhbiBvbmUgY29weSBvZiB0aGlzIHN1Ym1pc3Npb24gZm9yCnB1cnBvc2VzIG9mIHNlY3VyaXR5LCBiYWNrLXVwIGFuZCBwcmVzZXJ2YXRpb24uCgpZb3UgcmVwcmVzZW50IHRoYXQgdGhlIHN1Ym1pc3Npb24gaXMgeW91ciBvcmlnaW5hbCB3b3JrLCBhbmQgdGhhdCB5b3UgaGF2ZQp0aGUgcmlnaHQgdG8gZ3JhbnQgdGhlIHJpZ2h0cyBjb250YWluZWQgaW4gdGhpcyBsaWNlbnNlLiBZb3UgYWxzbyByZXByZXNlbnQKdGhhdCB5b3VyIHN1Ym1pc3Npb24gZG9lcyBub3QsIHRvIHRoZSBiZXN0IG9mIHlvdXIga25vd2xlZGdlLCBpbmZyaW5nZSB1cG9uCmFueW9uZSdzIGNvcHlyaWdodC4KCklmIHRoZSBzdWJtaXNzaW9uIGNvbnRhaW5zIG1hdGVyaWFsIGZvciB3aGljaCB5b3UgZG8gbm90IGhvbGQgY29weXJpZ2h0LAp5b3UgcmVwcmVzZW50IHRoYXQgeW91IGhhdmUgb2J0YWluZWQgdGhlIHVucmVzdHJpY3RlZCBwZXJtaXNzaW9uIG9mIHRoZQpjb3B5cmlnaHQgb3duZXIgdG8gZ3JhbnQgRFNVIHRoZSByaWdodHMgcmVxdWlyZWQgYnkgdGhpcyBsaWNlbnNlLCBhbmQgdGhhdApzdWNoIHRoaXJkLXBhcnR5IG93bmVkIG1hdGVyaWFsIGlzIGNsZWFybHkgaWRlbnRpZmllZCBhbmQgYWNrbm93bGVkZ2VkCndpdGhpbiB0aGUgdGV4dCBvciBjb250ZW50IG9mIHRoZSBzdWJtaXNzaW9uLgoKSUYgVEhFIFNVQk1JU1NJT04gSVMgQkFTRUQgVVBPTiBXT1JLIFRIQVQgSEFTIEJFRU4gU1BPTlNPUkVEIE9SIFNVUFBPUlRFRApCWSBBTiBBR0VOQ1kgT1IgT1JHQU5JWkFUSU9OIE9USEVSIFRIQU4gRFNVLCBZT1UgUkVQUkVTRU5UIFRIQVQgWU9VIEhBVkUKRlVMRklMTEVEIEFOWSBSSUdIVCBPRiBSRVZJRVcgT1IgT1RIRVIgT0JMSUdBVElPTlMgUkVRVUlSRUQgQlkgU1VDSApDT05UUkFDVCBPUiBBR1JFRU1FTlQuCgpEU1Ugd2lsbCBjbGVhcmx5IGlkZW50aWZ5IHlvdXIgbmFtZShzKSBhcyB0aGUgYXV0aG9yKHMpIG9yIG93bmVyKHMpIG9mIHRoZQpzdWJtaXNzaW9uLCBhbmQgd2lsbCBub3QgbWFrZSBhbnkgYWx0ZXJhdGlvbiwgb3RoZXIgdGhhbiBhcyBhbGxvd2VkIGJ5IHRoaXMKbGljZW5zZSwgdG8geW91ciBzdWJtaXNzaW9uLgo=

Publicaciones similares