DC FieldValueLanguage
dc.contributor.authorGhilezan, Silviaen_US
dc.contributor.authorIvetić, Jelenaen_US
dc.contributor.authorSavić, Nenaden_US
dc.date.accessioned2020-11-25T11:38:22Z-
dc.date.available2020-11-25T11:38:22Z-
dc.date.issued2015-
dc.identifier.urihttp://researchrepository.mi.sanu.ac.rs/handle/123456789/4237-
dc.description.abstractThe size of a lambda term’s type assignment is traditionally interpreted as the number of involved typing rules, since that interpretation corresponds to the complexity of underlying logical proof. However, it can be also assessed using some finer-grained measures such as the number of involved type declarations, or even as the sum of the sizes of all types in involved type declarations. These quantitative properties of type assignments are relevant for implementation issues, e.g. for compiler construction. We propose a type assignment method that relies on the translation of a typeable lambda term to the corresponding term of the resource control lambda calculus. This calculus, introduced by Ghilezan et al. in [1], contains operators for variable duplication and erasing, and linear substitution, whereas its typed version corresponds to intuitionistic logic with explicit structural rules of contraction and thinning. We prove that the translation preserves the type of a term, and that all output resource control lambda terms are in theirγω-normal forms, meaning that resource control operators are put in optimal positions considering the size of type assignments. The translation output of a given lambda term is often syntactically more complex and therefore more rules need to be used for its type assignment in the target resource control calculus. However, we show that two finer grained measures decrease when types are assigned to terms satisfying a certain minimal level of complexity.en_US
dc.relationRepresentations of logical structures and formal languages and their application in computingen_US
dc.relationDevelopment of new information and communication technologies, based on advanced mathematical methods, with applications in medicine, telecommunications, power systems, protection of national heritage and educationen_US
dc.relationAdvanced Techniques of Cryptology, Image Processing and Computational Topology for Information Securityen_US
dc.titleAn optimisation of lambda type assignments via resource controlen_US
dc.typeConference Paperen_US
dc.relation.conferenceLAP 2015 - Logic and Applications, pp 21-22, September 20-24, 2015, Dubrovnik, Croatiaen_US
dc.identifier.urlhttp://imft.ftn.uns.ac.rs/math/cms/uploads/Main/LAP2015_book_of_abstracts.pdf-
dc.relation.grantno174026en_US
dc.relation.grantno44006en_US
dc.relation.grantno174008en_US
dc.relation.firstpage21-
dc.relation.lastpage22-
dc.description.rankM34-
item.cerifentitytypePublications-
item.fulltextNo Fulltext-
item.openairecristypehttp://purl.org/coar/resource_type/c_18cf-
item.openairetypeConference Paper-
item.grantfulltextnone-
crisitem.author.orcid0000-0003-2253-8285-
crisitem.project.projectURLhttp://www.mi.sanu.ac.rs/novi_sajt/research/projects/174026e.php-
crisitem.project.projectURLhttp://www.mi.sanu.ac.rs/novi_sajt/research/projects/044006e.php-
crisitem.project.projectURLhttp://www.mi.sanu.ac.rs/novi_sajt/research/projects/174008e.php-
crisitem.project.fundingProgramDirectorate for Social, Behavioral & Economic Sciences-
crisitem.project.fundingProgramNATIONAL HEART, LUNG, AND BLOOD INSTITUTE-
crisitem.project.fundingProgramDirectorate for Education & Human Resources-
crisitem.project.openAireinfo:eu-repo/grantAgreement/NSF/Directorate for Social, Behavioral & Economic Sciences/1740267-
crisitem.project.openAireinfo:eu-repo/grantAgreement/NIH/NATIONAL HEART, LUNG, AND BLOOD INSTITUTE/5R01HL044006-04-
crisitem.project.openAireinfo:eu-repo/grantAgreement/NSF/Directorate for Education & Human Resources/1740089-
Show simple item record

Page view(s)

48
checked on May 9, 2024

Google ScholarTM

Check


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.