Sustituciones explícitas y todo eso

Vista sencilla de ítem
dc.contributor.authorAyala Rincón, Mauriciospa
dc.contributor.authorMuñoz, Césarspa
dc.contributor.googlescholarAyala Rincón, Mauricio [hd3UcpsAAAAJ]spa
dc.contributor.orcidAyala Rincón, Mauricio [0000-0003-0089-3905]spa
dc.contributor.researchgateAyala Rincón, Mauricio [Mauricio-Ayala-Rincon]spa
dc.date.accessioned2020-10-27T00:21:41Z
dc.date.available2020-10-27T00:21:41Z
dc.date.issued2000-12-01
dc.description.abstractLos cálculos de sustitución explícitos son extensiones del cálculo donde el mecanismo de sustitución se internaliza en la teoría. Esta característica los hace adecuados para la implementación y el estudio teórico de herramientas basadas en lógica como lenguajes de programación fuertemente tipados y sistemas de asistente de prueba.spa
dc.description.abstractenglishExplicit substitution calculus are extensions of the calculus where the substitution mechanism is internalized into the theory. This feature makes them suitable for the implementation and theoretical study of logic-based tools such as strongly typed programming languages and test wizard systems.eng
dc.format.mimetypeapplication/pdfspa
dc.identifier.instnameinstname:Universidad Autónoma de Bucaramanga UNABspa
dc.identifier.issn2539-2115
dc.identifier.issn1657-2831
dc.identifier.repourlrepourl:https://repository.unab.edu.co
dc.identifier.urihttp://hdl.handle.net/20.500.12749/9084
dc.language.isospaspa
dc.publisherUniversidad Autónoma de Bucaramanga UNAB
dc.relationhttps://revistas.unab.edu.co/index.php/rcc/article/view/1128/1098
dc.relation.referencesM.Abadi,L.Cardelli,P.-L.Curien,andJ.-J.L evy.ExplicitSubstitutions.JournalofFunctionalProgramming,1(4):375{416,1991.
dc.relation.referencesM.Ayala-Rinc onandF.Kamareddine.Uni cationvia se-StyleofExplicitSubstitution.In2ndInternationalConferenceonPrinciplesandPracticeofDeclarativeProgramming,Montreal,Canada,September2000.ACMPress.
dc.relation.referencesH.P.Barendregt.TheLambdaCalculus:ItsSyntaxandSemantics(revisededition).NorthHolland,1984.
dc.relation.referencesH.P.Barendregt. -calculiwithtypes.HandbookofLogicinComputerScience,II,1992.
dc.relation.referencesB.Barras,S.Boutin,C.Cornes,J.Courant,J.C.Filliatre,E.Gim enez,H.Herbelin,G.Huet,C.Mu~noz,C.Murthy,C.Parent,C.Paulin,A.Sa bi,andB.Werner.TheCoqProofAssistantReferenceManual{VersionV6.1.TechnicalReport0203,INRIA,August1997.
dc.relation.referencesN.Bj rnerandC.Mu~noz.Absoluteexplicituni cation.Acceptedforpublication.Internationalcon-ferenceonRewritingTechniquesandApplications(RTA'2000),July2000.
dc.relation.referencesR.Bloo.PreservationofTerminationforExplicitSubstitution.PhDthesis,DepartmentofMathematicsandComputingScience,EindhovenUniversityofTechnology,1997
dc.relation.referencesR.BlooandK.H.Rose.Preservationofstrongnormalisationinnamedlambdacalculiwithexplicitsubstitutionandgarbagecollection.InProc.CSN-95:ComputerScienceintheNetherlands,November1995.
dc.relation.referencesD.Briaud.Higherorderuni cationasatypednarrowing.Technicalreport,CRINreport96-R-112,1996.
dc.relation.referencesA.Church.Anunsolvableproblemofelementarynumbertheory.AmericanJournalofMathematics,58:345{363,1936.
dc.relation.referencesA.Church.Aformulationofthesimpletheoryoftypes.JournalofSymbolicLogic,5:56{68,1940.
dc.relation.referencesA.Church.TheCalculiofLambda-Conversion.PrincetonUniversityPress,1941.
dc.relation.referencesH.CirsteaandC.Kirchner.CombiningHigher-OrderandFirst-OrderComputationUsingp-Calculus:TowardsaSemanticsofELAN.InD.M.GabbayandM.deRijke,editors,FrontiersofCombiningSystems2,StudiesonLogicandComputation,7,chapter6,pages95{121.ResearchStudiesPress/Wiley,1999.
dc.relation.referencesH.CirsteaandC.Kirchner.IntroductiontotheRewritingCalculus.RapportdeRecherche3818,INRIA,December1999.
dc.relation.referencesT.Coquand.UneTh eoriedeConstructions.Th esededoctorat,U.ParisVII,1985.
dc.relation.referencesT.CoquandandG.Huet.TheCalculusofConstructions.InformationandComputation,76:96{120,1988
dc.relation.referencesP.-L.Curien,T.Hardin,andJ.-J.L evy.Con uencePropertiesofWeakandStrongCalculiofExplicitSubstitutions.JournaloftheACM,43(2):362{397,1996.AlsoasRapportdeRechercheINRIA1617,1992.
dc.relation.referencesH.B.CurryandR.Feys.CombinatoryLogic,volume1.NorthHolland,1958.
dc.relation.referencesN.G.deBruijn.Lambda-CalculusNotationwithNamelessDummies,aToolforAutomaticFormulaManipulation,withApplicationtotheChurch-RosserTheorem.Indag.Mat.,34(5):381{392,1972.
dc.relation.referencesG.Dowek.Acompleteproofsynthesismethodfortypesystemsofthecube.JournalofLogicandComputation,3(3):287{315,June1993.
dc.relation.referencesG.Dowek,T.Hardin,andC.Kirchner.Higher-orderUni cationviaExplicitSubstitutions.InformationandComputation,157(1/2):183{235,2000.
dc.relation.referencesG.Dowek,T.Hardin,C.Kirchner,andF.Pfenning.Uni cationviaexplicitsubstitutions:Thecaseofhigher-orderpatterns.InM.Maher,editor,ProceedingsoftheJointInternationalConferenceandSymposiumonLogicProgramming,Bonn,Germany,September1996.MITPress.
dc.relation.referencesW.Farmer.AUni cationAlgorithmforSecond-OrderMonadicTerms.AnnalsofPureandAppliedLogic,39:131{174,1988.
dc.relation.referencesM.C.F.Ferreira,D.Kesner,andL.Puel.Lambda-calculiwithexplicitsubstitutionsandcompositionwhichpreservebeta-strongnormalization.InMichaelHanusandMarioRodr guez-Artalejo,editors,AlgebraicandLogicProgramming,5thInternationalConference,ALP'96,volume1139ofLNCS,pages284{298,Aachen,Germany,25{27September1996.Springer.
dc.relation.referencesJeanYvesGirard.Interpr etationFonctionelleet EliminationdesCompuresdel'Arithm eticd'OrdreSup erieur.Th esededoctorat,Universit eParisVII,1972.
dc.relation.referencesW.Goldfarb.TheUndecidabilityoftheSecond-OrderUni cationProblem.TheoreticalComputerScience,13(2):225{230,1981.
dc.relation.referencesM.J.C.GordonandT.F.Melham.IntroductiontoHOL:ATheoremProvingEnvironmentforHigherOrderLogic.CambridgeUniversityPress,1993.
dc.relation.referencesB.Guillaume.The se-calculusDoesNotPreserveStrongNormalization.JournalofFunctionalPro-gramming,1999.Toappear.
dc.relation.referencesR.Harper,F.Honsell,andG.Plotkin.Aframeworkforde ninglogics.JournaloftheAssociationforComputingMachinery,40(1):143{184,1993.
dc.relation.referencesJ.R.Hindley.BasicSimpleTypeTheory.Number42inCambridgeTractsinTheoreticalComputerScience.CambridgeUniversityPress,1997.
dc.relation.referencesG.Huet.AUni cationAlgorithmforTyped -Calculus.TheoreticalComputerScience,1:27{57,1975.
dc.relation.referencesF.KamareddineandA.R os.A -calculus aladeBruijnwithExplicitSubstitutions.InProc.ofPLILP'95,volume982ofLNCS,pages45{62.Springer,1995.
dc.relation.referencesF.KamareddineandA.R os.Extendinga -calculuswithExplicitSubstitutionwhichPreservesStrongNormalisationintoaCon uentCalculusonOpenTerms.JournalofFunctionalProgramming,7:395{420,1997.
dc.relation.referencesF.KamareddineandA.R os.Relatingthe -and s-StylesofExplicitSubstitutions.JournalofLogicandComputation,10(3):349{380,2000.
dc.relation.referencesD.Kesner.Con uencepropertiesofextensionalandnon-extensional -calculiwithexplicitsubstitu-tions(extendedabstract).InH.Ganzinger,editor,ProceedingsoftheSeventhInternationalConfer-enceonRewritingTechniquesandApplications(RTA-96),volume1103ofLNCS,pages184{199,NewBrunswick,NewJersey,1996.Springer-Verlag.
dc.relation.referencesC.KirchnerandC.Ringeissen.Higher-orderEquationalUni cationviaExplicitSubstitutions.InProc.AlgebraicandLogicProgramming,volume1298ofLNCS,pages61{75.Springer,1997
dc.relation.referencesS.C.Kleene. -de nabilityandrecursiveness.DukeMathematicalJournal,2:340{353,1936
dc.relation.referencesP.Lescanne.From to aJourneyThroughCalculiofExplicitSubstitutions.InProceedingsofthe21stAnnualACMSIGPLAN-SIGACTSymposiumonPrinciplesofProgrammingLanguages,pages60{69,January1994.
dc.relation.referencesP.LescanneandJ.Rouyer-Degli.ExplicitsubstitutionswithdeBruijn'slevels.InJ.Hsiang,edi-tor,ProceedingsoftheInternationalConferenceonRewritingTechniquesandApplications(RTA-95),volume914ofLNCS,pages294{308,ChapelHill,NorthCarolina,1995.Springer-Verla
dc.relation.referencesP.-A.Melli es.Typed -calculiwithexplicitsubstitutionsmaynotterminateinProceedingsofTLCA'95.LNCS,902,1995
dc.relation.referencesD.Miller. Prolog:AnIntroductiontotheLanguageanditsLogic.Draft,DepartmentofComputerScienceandEngineering,ThePennsylvaniaStateUniversity,1998.
dc.relation.referencesRobinMilner,M.Tofte,andR.Harper.TheDe nitionofStandardML.MITPress,Cambridge,MA,1991.
dc.relation.referencesC.Mu~noz.Con uenceandpreservationofstrongnormalisationinanexplicitsubstitutionscalculus(extendedabstract).InProceedingsoftheEleventhAnnualIEEESymposiumonLogicinComputerScience,pages440{447,NewBrunswick,NewJersey,July1996.IEEEComputerSocietyPress.19
dc.relation.referencesC.Mu~noz.Aleft-linearvariantof .InProc.InternationalConferencePLILP/ALP/HOA'97,volume1298ofLNCS,pages224{234,Southampton(England),September1997.Springer.
dc.relation.referencesC.Mu~noz.Uncalculdesubstitutionspourlarepr esentationdepreuvespartiellesenth eoriedetypes.PhDthesis,Universit eParis7,1997.EnglishversioninRapportderechercheINRIARR-3309,1997.
dc.relation.referencesC.Mu~noz.Dependenttypesandexplicitsubstitutions.AcceptedforpublicationinthejournalMathe-maticalStructuresinComputerScience.ItalsoappearsasreportNASA/CR-1999-209722ICASENo.99-43.,1999.
dc.relation.referencesC.Mu~noz.Proof-termsynthesisondependent-typesystemsviaexplicitsubstitutions.AcceptedforpublicationinthejournalTheoreticalComputerScience.ItalsoappearsasreportNASA/CR-1999-209730ICASENo.99-47.andwaspresentedintheInternationalWorkshoponExplicitSubstitutions:TheoryandApplicationstoProgramsandProofs-WESTAPP98,Tsukuba,Japan,2000.
dc.relation.referencesG.Nadathur.A ne-grainednotationforlambdatermsanditsuseinintensionaloperations.TechnicalReportTR-96-13,DepartmentofComputerScience,UniversityofChicago,May301996.AcceptedforpublicationinJournalofFunctionalandLogicProgramming.
dc.relation.referencesG.NadathurandD.S.Wilson.ANotationforLambdaTermsAGeneralizationofEnvironments.TheoreticalComputerScience,198:49{98,1998.
dc.relation.referencesR.P.Nederpelt,J.H.Geuvers,andR.C.deVrijer.SelectedpapersonAutomath.North-Holland,Amsterdam,1994.
dc.relation.referencesS.Owre,J.M.Rushby,andN.Shankar.PVS:Aprototypeveri cationsystem.InD.Kapur,editor,11thInternationalConferenceonAutomatedDeduction(CADE),volume607ofLectureNotesinArti cialIntelligence,pages748{752,Saratoga,NY,June1992.Springer-Verlag.
dc.relation.referencesF.PfenningandC.Sch urmann.Twelfuser'sguide,1.2.edition.TechnicalReportCMU-CS-1998-173,CarnegieMellonUniversity,September1998.
dc.relation.referencesC.Prehofer.ProgressinTheoreticalComputerScience.InR.V.Book,editor,SolvingHigher-OrderEquations:FromLogictoProgramming.Birkh auser,1997.
dc.relation.referencesC.Prehofer.ProgressinTheoreticalComputerScience.InR.V.Book,editor,SolvingHigher-OrderEquations:FromLogictoProgramming.Birkh auser,1997.
dc.relation.referencesA.R os.Contributions al' etudede -calculsavecdessubstitutionsexplicites.Th esededoctorat,Universit eParisVII,1993.
dc.relation.referencesJ.A.Robinson.AMachine-orientedLogicBasedontheResolutionPrinciple.JournaloftheACM,12(1):23{41,January1965.
dc.relation.referencesK.H.Rose.ExplicitSubstitution-Tutorial&Survey.BRICS,LectureSeriesLS-96-3,DepartmentofComputerScience,UniversityofAarhus,1996.
dc.relation.referencesW.SnyderandJ.Gallier.Higher-OrderUni cationRevisited:CompleteSetsofTransformations.JournalofSymbolicComputation,8:101{140,1989.
dc.relation.referencesA.N.WhiteheadandB.Russell.PrincipiaMathematica.CambridgeUniversityPress,Cambridge,revisededition,1925{1927.Threevolumes.The rsteditionwaspublished1910{1913.20
dc.relation.urihttps://revistas.unab.edu.co/index.php/rcc/article/view/1128
dc.rightsDerechos de autor 2000 Revista Colombiana de Computación
dc.rights.accessrightsinfo:eu-repo/semantics/openAccessspa
dc.rights.creativecommonsAtribución-NoComercial-SinDerivadas 2.5 Colombia*
dc.rights.urihttp://creativecommons.org/licenses/by-nc-sa/4.0/*
dc.rights.urihttp://creativecommons.org/licenses/by-nc-nd/2.5/co/
dc.sourceRevista Colombiana de Computación; Vol. 1 Núm. 1 (2000): Revista Colombiana de Computación; 46-72
dc.subjectInnovaciones tecnológicas
dc.subjectCiencia de los computadores
dc.subjectDesarrollo de tecnología
dc.subjectIngeniería de sistemas
dc.subjectInvestigaciones
dc.subjectTecnologías de la información y las comunicaciones
dc.subjectTIC´s
dc.subject.keywordsTechnological innovationseng
dc.subject.keywordsComputer scienceeng
dc.subject.keywordsTechnology developmenteng
dc.subject.keywordsSystems engineeringeng
dc.subject.keywordsInvestigationseng
dc.subject.keywordsInformation and communication technologieseng
dc.subject.keywordsICT'seng
dc.subject.keywordsClean Sustitucióneng
dc.subject.keywordsOrden superioreng
dc.subject.keywordsTeoría de la reescrituraeng
dc.subject.keywordsProgramacioneng
dc.subject.lembInnovaciones tecnológicasspa
dc.subject.lembCiencias de la Computaciónspa
dc.subject.lembDesarrollo tecnológicospa
dc.subject.lembIngeniería de sistemasspa
dc.subject.lembInvestigacionesspa
dc.subject.proposalSustitución explícitaspa
dc.subject.proposalOrden superiorspa
dc.subject.proposalTeoría de la reescrituraspa
dc.subject.proposalProgramaciónspa
dc.titleSustituciones explícitas y todo esospa
dc.title.translatedExplicit substitions and all thateng
dc.type.coarhttp://purl.org/coar/resource_type/c_7a1f
dc.type.driverinfo:eu-repo/semantics/article
dc.type.hasversionInfo:eu-repo/semantics/publishedVersion
dc.type.hasversioninfo:eu-repo/semantics/acceptedVersion
dc.type.localArtículospa
dc.type.redcolhttp://purl.org/redcol/resource_type/CJournalArticle

Archivos

Bloque original

Mostrando 1 - 1 de 1
Miniatura
Nombre:
Ayala Rincon, Mauricio_Sustituciones explícitas y todo eso.pdf
Tamaño:
360.32 KB
Formato:
Adobe Portable Document Format
Descripción:
Artículo
Descargar

Colecciones

Revista Colombiana de Computación