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...
- 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
- http://creativecommons.org/licenses/by-nc-nd/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 |
Tesis/Trabajo de grado - Monografía - Pregrado |
| 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.coarversion.spa.fl_str_mv |
http://purl.org/coar/version/c_b1a7d7d4d402bcce |
| dc.type.driver.spa.fl_str_mv |
info:eu-repo/semantics/bachelorThesis |
| dc.type.version.spa.fl_str_mv |
info:eu-repo/semantics/draft |
| 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.uri.*.fl_str_mv |
http://creativecommons.org/licenses/by-nc-nd/2.5/co/ |
| dc.rights.uri.spa.fl_str_mv |
https://creativecommons.org/licenses/by-nc-sa/4.0/ |
| dc.rights.accessrights.spa.fl_str_mv |
info:eu-repo/semantics/openAccess |
| dc.rights.accessrights.*.fl_str_mv |
Atribución-NoComercial-CompartirIgual 2.5 Colombia (CC BY-NC-SA 2.5 CO) |
| dc.rights.coar.spa.fl_str_mv |
http://purl.org/coar/access_right/c_abf2 |
| rights_invalid_str_mv |
http://creativecommons.org/licenses/by-nc-nd/2.5/co/ https://creativecommons.org/licenses/by-nc-sa/4.0/ Atribución-NoComercial-CompartirIgual 2.5 Colombia (CC BY-NC-SA 2.5 CO) http://purl.org/coar/access_right/c_abf2 |
| eu_rights_str_mv |
openAccess |
| dc.format.extent.spa.fl_str_mv |
32 |
| dc.format.mimetype.spa.fl_str_mv |
application/pdf |
| dc.publisher.spa.fl_str_mv |
Universidad de Antioquia |
| dc.publisher.place.spa.fl_str_mv |
Medellín, Colombia |
| dc.publisher.faculty.spa.fl_str_mv |
Facultad de Ciencias Exactas y Naturales. Matemáticas |
| institution |
Universidad de Antioquia |
| bitstream.url.fl_str_mv |
https://bibliotecadigital.udea.edu.co/bitstreams/cbe905f9-4f4b-4bf2-8771-ea29784d090c/download https://bibliotecadigital.udea.edu.co/bitstreams/2076353f-b66f-49bf-8d22-4c079a92fe42/download https://bibliotecadigital.udea.edu.co/bitstreams/17ab5bc2-2558-4b63-841a-005a880248c9/download https://bibliotecadigital.udea.edu.co/bitstreams/c8f50793-170b-43d0-8f5e-f6e21b336b8c/download https://bibliotecadigital.udea.edu.co/bitstreams/0876eed0-90c7-447a-9d1d-ea8e8daba798/download |
| bitstream.checksum.fl_str_mv |
472dde3aa854eae752525ac5f7fffe78 b88b088d9957e670ce3b3fbe2eedbc13 8a4605be74aa9ea9d79846c1fba20a33 d28638245d5c951ac2a119b7031ea81f c90f075e8b216cbf904a0e7398301f0d |
| bitstream.checksumAlgorithm.fl_str_mv |
MD5 MD5 MD5 MD5 MD5 |
| repository.name.fl_str_mv |
Repositorio Institucional de la Universidad de Antioquia |
| repository.mail.fl_str_mv |
aplicacionbibliotecadigitalbiblioteca@udea.edu.co |
| _version_ |
1851052535574429696 |
| 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.PregradoMatemático32application/pdfengUniversidad de AntioquiaMedellín, ColombiaFacultad de Ciencias Exactas y Naturales. Matemáticashttp://creativecommons.org/licenses/by-nc-nd/2.5/co/https://creativecommons.org/licenses/by-nc-sa/4.0/info:eu-repo/semantics/openAccessAtribución-NoComercial-CompartirIgual 2.5 Colombia (CC BY-NC-SA 2.5 CO)http://purl.org/coar/access_right/c_abf2Lambda 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 typesTesis/Trabajo de grado - Monografía - Pregradohttp://purl.org/coar/resource_type/c_7a1fhttps://purl.org/redcol/resource_type/TPhttp://purl.org/coar/version/c_b1a7d7d4d402bcceinfo:eu-repo/semantics/bachelorThesisinfo:eu-repo/semantics/draftPublicationORIGINALPinillaAlejandro_2022_SimplyTypedLambda.pdfPinillaAlejandro_2022_SimplyTypedLambda.pdfTrabajo de grado de pregradoapplication/pdf420153https://bibliotecadigital.udea.edu.co/bitstreams/cbe905f9-4f4b-4bf2-8771-ea29784d090c/download472dde3aa854eae752525ac5f7fffe78MD51trueAnonymousREADCC-LICENSElicense_rdflicense_rdfapplication/rdf+xml; charset=utf-8823https://bibliotecadigital.udea.edu.co/bitstreams/2076353f-b66f-49bf-8d22-4c079a92fe42/downloadb88b088d9957e670ce3b3fbe2eedbc13MD52falseAnonymousREADLICENSElicense.txtlicense.txttext/plain; charset=utf-81748https://bibliotecadigital.udea.edu.co/bitstreams/17ab5bc2-2558-4b63-841a-005a880248c9/download8a4605be74aa9ea9d79846c1fba20a33MD53falseAnonymousREADTEXTPinillaAlejandro_2022_SimplyTypedLambda.pdf.txtPinillaAlejandro_2022_SimplyTypedLambda.pdf.txtExtracted texttext/plain61773https://bibliotecadigital.udea.edu.co/bitstreams/c8f50793-170b-43d0-8f5e-f6e21b336b8c/downloadd28638245d5c951ac2a119b7031ea81fMD54falseAnonymousREADTHUMBNAILPinillaAlejandro_2022_SimplyTypedLambda.pdf.jpgPinillaAlejandro_2022_SimplyTypedLambda.pdf.jpgGenerated Thumbnailimage/jpeg5718https://bibliotecadigital.udea.edu.co/bitstreams/0876eed0-90c7-447a-9d1d-ea8e8daba798/downloadc90f075e8b216cbf904a0e7398301f0dMD55falseAnonymousREAD10495/27314oai:bibliotecadigital.udea.edu.co:10495/273142025-03-26 23:55:54.128http://creativecommons.org/licenses/by-nc-nd/2.5/co/open.accesshttps://bibliotecadigital.udea.edu.coRepositorio Institucional de la Universidad de Antioquiaaplicacionbibliotecadigitalbiblioteca@udea.edu.coTk9URTogUExBQ0UgWU9VUiBPV04gTElDRU5TRSBIRVJFClRoaXMgc2FtcGxlIGxpY2Vuc2UgaXMgcHJvdmlkZWQgZm9yIGluZm9ybWF0aW9uYWwgcHVycG9zZXMgb25seS4KCk5PTi1FWENMVVNJVkUgRElTVFJJQlVUSU9OIExJQ0VOU0UKCkJ5IHNpZ25pbmcgYW5kIHN1Ym1pdHRpbmcgdGhpcyBsaWNlbnNlLCB5b3UgKHRoZSBhdXRob3Iocykgb3IgY29weXJpZ2h0Cm93bmVyKSBncmFudHMgdG8gRFNwYWNlIFVuaXZlcnNpdHkgKERTVSkgdGhlIG5vbi1leGNsdXNpdmUgcmlnaHQgdG8gcmVwcm9kdWNlLAp0cmFuc2xhdGUgKGFzIGRlZmluZWQgYmVsb3cpLCBhbmQvb3IgZGlzdHJpYnV0ZSB5b3VyIHN1Ym1pc3Npb24gKGluY2x1ZGluZwp0aGUgYWJzdHJhY3QpIHdvcmxkd2lkZSBpbiBwcmludCBhbmQgZWxlY3Ryb25pYyBmb3JtYXQgYW5kIGluIGFueSBtZWRpdW0sCmluY2x1ZGluZyBidXQgbm90IGxpbWl0ZWQgdG8gYXVkaW8gb3IgdmlkZW8uCgpZb3UgYWdyZWUgdGhhdCBEU1UgbWF5LCB3aXRob3V0IGNoYW5naW5nIHRoZSBjb250ZW50LCB0cmFuc2xhdGUgdGhlCnN1Ym1pc3Npb24gdG8gYW55IG1lZGl1bSBvciBmb3JtYXQgZm9yIHRoZSBwdXJwb3NlIG9mIHByZXNlcnZhdGlvbi4KCllvdSBhbHNvIGFncmVlIHRoYXQgRFNVIG1heSBrZWVwIG1vcmUgdGhhbiBvbmUgY29weSBvZiB0aGlzIHN1Ym1pc3Npb24gZm9yCnB1cnBvc2VzIG9mIHNlY3VyaXR5LCBiYWNrLXVwIGFuZCBwcmVzZXJ2YXRpb24uCgpZb3UgcmVwcmVzZW50IHRoYXQgdGhlIHN1Ym1pc3Npb24gaXMgeW91ciBvcmlnaW5hbCB3b3JrLCBhbmQgdGhhdCB5b3UgaGF2ZQp0aGUgcmlnaHQgdG8gZ3JhbnQgdGhlIHJpZ2h0cyBjb250YWluZWQgaW4gdGhpcyBsaWNlbnNlLiBZb3UgYWxzbyByZXByZXNlbnQKdGhhdCB5b3VyIHN1Ym1pc3Npb24gZG9lcyBub3QsIHRvIHRoZSBiZXN0IG9mIHlvdXIga25vd2xlZGdlLCBpbmZyaW5nZSB1cG9uCmFueW9uZSdzIGNvcHlyaWdodC4KCklmIHRoZSBzdWJtaXNzaW9uIGNvbnRhaW5zIG1hdGVyaWFsIGZvciB3aGljaCB5b3UgZG8gbm90IGhvbGQgY29weXJpZ2h0LAp5b3UgcmVwcmVzZW50IHRoYXQgeW91IGhhdmUgb2J0YWluZWQgdGhlIHVucmVzdHJpY3RlZCBwZXJtaXNzaW9uIG9mIHRoZQpjb3B5cmlnaHQgb3duZXIgdG8gZ3JhbnQgRFNVIHRoZSByaWdodHMgcmVxdWlyZWQgYnkgdGhpcyBsaWNlbnNlLCBhbmQgdGhhdApzdWNoIHRoaXJkLXBhcnR5IG93bmVkIG1hdGVyaWFsIGlzIGNsZWFybHkgaWRlbnRpZmllZCBhbmQgYWNrbm93bGVkZ2VkCndpdGhpbiB0aGUgdGV4dCBvciBjb250ZW50IG9mIHRoZSBzdWJtaXNzaW9uLgoKSUYgVEhFIFNVQk1JU1NJT04gSVMgQkFTRUQgVVBPTiBXT1JLIFRIQVQgSEFTIEJFRU4gU1BPTlNPUkVEIE9SIFNVUFBPUlRFRApCWSBBTiBBR0VOQ1kgT1IgT1JHQU5JWkFUSU9OIE9USEVSIFRIQU4gRFNVLCBZT1UgUkVQUkVTRU5UIFRIQVQgWU9VIEhBVkUKRlVMRklMTEVEIEFOWSBSSUdIVCBPRiBSRVZJRVcgT1IgT1RIRVIgT0JMSUdBVElPTlMgUkVRVUlSRUQgQlkgU1VDSApDT05UUkFDVCBPUiBBR1JFRU1FTlQuCgpEU1Ugd2lsbCBjbGVhcmx5IGlkZW50aWZ5IHlvdXIgbmFtZShzKSBhcyB0aGUgYXV0aG9yKHMpIG9yIG93bmVyKHMpIG9mIHRoZQpzdWJtaXNzaW9uLCBhbmQgd2lsbCBub3QgbWFrZSBhbnkgYWx0ZXJhdGlvbiwgb3RoZXIgdGhhbiBhcyBhbGxvd2VkIGJ5IHRoaXMKbGljZW5zZSwgdG8geW91ciBzdWJtaXNzaW9uLgo= |