Sustituciones explícitas y todo eso

Los 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...

Full description

Autores:
Ayala Rincón, Mauricio
Muñoz, César
Tipo de recurso:
Trabajo de grado de pregrado
Fecha de publicación:
2000
Institución:
Universidad Autónoma de Bucaramanga - UNAB
Repositorio:
Repositorio UNAB
Idioma:
spa
OAI Identifier:
oai:repository.unab.edu.co:20.500.12749/9084
Acceso en línea:
http://hdl.handle.net/20.500.12749/9084
Palabra clave:
Innovaciones tecnológicas
Ciencia de los computadores
Desarrollo de tecnología
Ingeniería de sistemas
Investigaciones
Tecnologías de la información y las comunicaciones
TIC´s
Technological innovations
Computer science
Technology development
Systems engineering
Investigations
Information and communication technologies
ICT's
Clean Sustitución
Orden superior
Teoría de la reescritura
Programacion
Innovaciones tecnológicas
Ciencias de la Computación
Desarrollo tecnológico
Ingeniería de sistemas
Investigaciones
Sustitución explícita
Orden superior
Teoría de la reescritura
Programación
Rights
License
Derechos de autor 2000 Revista Colombiana de Computación
id UNAB2_01c85e4abb096224e1c6fa9523b67668
oai_identifier_str oai:repository.unab.edu.co:20.500.12749/9084
network_acronym_str UNAB2
network_name_str Repositorio UNAB
repository_id_str
dc.title.spa.fl_str_mv Sustituciones explícitas y todo eso
dc.title.translated.eng.fl_str_mv Explicit substitions and all that
title Sustituciones explícitas y todo eso
spellingShingle Sustituciones explícitas y todo eso
Innovaciones tecnológicas
Ciencia de los computadores
Desarrollo de tecnología
Ingeniería de sistemas
Investigaciones
Tecnologías de la información y las comunicaciones
TIC´s
Technological innovations
Computer science
Technology development
Systems engineering
Investigations
Information and communication technologies
ICT's
Clean Sustitución
Orden superior
Teoría de la reescritura
Programacion
Innovaciones tecnológicas
Ciencias de la Computación
Desarrollo tecnológico
Ingeniería de sistemas
Investigaciones
Sustitución explícita
Orden superior
Teoría de la reescritura
Programación
title_short Sustituciones explícitas y todo eso
title_full Sustituciones explícitas y todo eso
title_fullStr Sustituciones explícitas y todo eso
title_full_unstemmed Sustituciones explícitas y todo eso
title_sort Sustituciones explícitas y todo eso
dc.creator.fl_str_mv Ayala Rincón, Mauricio
Muñoz, César
dc.contributor.author.spa.fl_str_mv Ayala Rincón, Mauricio
Muñoz, César
dc.contributor.googlescholar.spa.fl_str_mv Ayala Rincón, Mauricio [hd3UcpsAAAAJ]
dc.contributor.orcid.spa.fl_str_mv Ayala Rincón, Mauricio [0000-0003-0089-3905]
dc.contributor.researchgate.spa.fl_str_mv Ayala Rincón, Mauricio [Mauricio-Ayala-Rincon]
dc.subject.none.fl_str_mv Innovaciones tecnológicas
Ciencia de los computadores
Desarrollo de tecnología
Ingeniería de sistemas
Investigaciones
Tecnologías de la información y las comunicaciones
TIC´s
topic Innovaciones tecnológicas
Ciencia de los computadores
Desarrollo de tecnología
Ingeniería de sistemas
Investigaciones
Tecnologías de la información y las comunicaciones
TIC´s
Technological innovations
Computer science
Technology development
Systems engineering
Investigations
Information and communication technologies
ICT's
Clean Sustitución
Orden superior
Teoría de la reescritura
Programacion
Innovaciones tecnológicas
Ciencias de la Computación
Desarrollo tecnológico
Ingeniería de sistemas
Investigaciones
Sustitución explícita
Orden superior
Teoría de la reescritura
Programación
dc.subject.keywords.eng.fl_str_mv Technological innovations
Computer science
Technology development
Systems engineering
Investigations
Information and communication technologies
ICT's
Clean Sustitución
Orden superior
Teoría de la reescritura
Programacion
dc.subject.lemb.spa.fl_str_mv Innovaciones tecnológicas
Ciencias de la Computación
Desarrollo tecnológico
Ingeniería de sistemas
Investigaciones
dc.subject.proposal.spa.fl_str_mv Sustitución explícita
Orden superior
Teoría de la reescritura
Programación
description Los 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.
publishDate 2000
dc.date.issued.none.fl_str_mv 2000-12-01
dc.date.accessioned.none.fl_str_mv 2020-10-27T00:21:41Z
dc.date.available.none.fl_str_mv 2020-10-27T00:21:41Z
dc.type.coar.fl_str_mv http://purl.org/coar/resource_type/c_2df8fbb1
dc.type.coarversion.fl_str_mv http://purl.org/coar/version/c_970fb48d4fbd8a85
dc.type.driver.none.fl_str_mv info:eu-repo/semantics/article
dc.type.local.spa.fl_str_mv Artículo
dc.type.coar.none.fl_str_mv http://purl.org/coar/resource_type/c_7a1f
dc.type.redcol.none.fl_str_mv http://purl.org/redcol/resource_type/CJournalArticle
format http://purl.org/coar/resource_type/c_7a1f
dc.identifier.issn.none.fl_str_mv 2539-2115
1657-2831
dc.identifier.uri.none.fl_str_mv http://hdl.handle.net/20.500.12749/9084
dc.identifier.instname.spa.fl_str_mv instname:Universidad Autónoma de Bucaramanga UNAB
dc.identifier.repourl.none.fl_str_mv repourl:https://repository.unab.edu.co
identifier_str_mv 2539-2115
1657-2831
instname:Universidad Autónoma de Bucaramanga UNAB
repourl:https://repository.unab.edu.co
url http://hdl.handle.net/20.500.12749/9084
dc.language.iso.spa.fl_str_mv spa
language spa
dc.relation.none.fl_str_mv https://revistas.unab.edu.co/index.php/rcc/article/view/1128/1098
dc.relation.uri.none.fl_str_mv https://revistas.unab.edu.co/index.php/rcc/article/view/1128
dc.relation.references.none.fl_str_mv M.Abadi,L.Cardelli,P.-L.Curien,andJ.-J.L evy.ExplicitSubstitutions.JournalofFunctionalProgramming,1(4):375{416,1991.
M.Ayala-Rinc onandF.Kamareddine.Uni cationvia se-StyleofExplicitSubstitution.In2ndInternationalConferenceonPrinciplesandPracticeofDeclarativeProgramming,Montreal,Canada,September2000.ACMPress.
H.P.Barendregt.TheLambdaCalculus:ItsSyntaxandSemantics(revisededition).NorthHolland,1984.
H.P.Barendregt. -calculiwithtypes.HandbookofLogicinComputerScience,II,1992.
B.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.
N.Bj rnerandC.Mu~noz.Absoluteexplicituni cation.Acceptedforpublication.Internationalcon-ferenceonRewritingTechniquesandApplications(RTA'2000),July2000.
R.Bloo.PreservationofTerminationforExplicitSubstitution.PhDthesis,DepartmentofMathematicsandComputingScience,EindhovenUniversityofTechnology,1997
R.BlooandK.H.Rose.Preservationofstrongnormalisationinnamedlambdacalculiwithexplicitsubstitutionandgarbagecollection.InProc.CSN-95:ComputerScienceintheNetherlands,November1995.
D.Briaud.Higherorderuni cationasatypednarrowing.Technicalreport,CRINreport96-R-112,1996.
A.Church.Anunsolvableproblemofelementarynumbertheory.AmericanJournalofMathematics,58:345{363,1936.
A.Church.Aformulationofthesimpletheoryoftypes.JournalofSymbolicLogic,5:56{68,1940.
A.Church.TheCalculiofLambda-Conversion.PrincetonUniversityPress,1941.
H.CirsteaandC.Kirchner.CombiningHigher-OrderandFirst-OrderComputationUsingp-Calculus:TowardsaSemanticsofELAN.InD.M.GabbayandM.deRijke,editors,FrontiersofCombiningSystems2,StudiesonLogicandComputation,7,chapter6,pages95{121.ResearchStudiesPress/Wiley,1999.
H.CirsteaandC.Kirchner.IntroductiontotheRewritingCalculus.RapportdeRecherche3818,INRIA,December1999.
T.Coquand.UneTh eoriedeConstructions.Th esededoctorat,U.ParisVII,1985.
T.CoquandandG.Huet.TheCalculusofConstructions.InformationandComputation,76:96{120,1988
P.-L.Curien,T.Hardin,andJ.-J.L evy.Con uencePropertiesofWeakandStrongCalculiofExplicitSubstitutions.JournaloftheACM,43(2):362{397,1996.AlsoasRapportdeRechercheINRIA1617,1992.
H.B.CurryandR.Feys.CombinatoryLogic,volume1.NorthHolland,1958.
N.G.deBruijn.Lambda-CalculusNotationwithNamelessDummies,aToolforAutomaticFormulaManipulation,withApplicationtotheChurch-RosserTheorem.Indag.Mat.,34(5):381{392,1972.
G.Dowek.Acompleteproofsynthesismethodfortypesystemsofthecube.JournalofLogicandComputation,3(3):287{315,June1993.
G.Dowek,T.Hardin,andC.Kirchner.Higher-orderUni cationviaExplicitSubstitutions.InformationandComputation,157(1/2):183{235,2000.
G.Dowek,T.Hardin,C.Kirchner,andF.Pfenning.Uni cationviaexplicitsubstitutions:Thecaseofhigher-orderpatterns.InM.Maher,editor,ProceedingsoftheJointInternationalConferenceandSymposiumonLogicProgramming,Bonn,Germany,September1996.MITPress.
W.Farmer.AUni cationAlgorithmforSecond-OrderMonadicTerms.AnnalsofPureandAppliedLogic,39:131{174,1988.
M.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.
JeanYvesGirard.Interpr etationFonctionelleet EliminationdesCompuresdel'Arithm eticd'OrdreSup erieur.Th esededoctorat,Universit eParisVII,1972.
W.Goldfarb.TheUndecidabilityoftheSecond-OrderUni cationProblem.TheoreticalComputerScience,13(2):225{230,1981.
M.J.C.GordonandT.F.Melham.IntroductiontoHOL:ATheoremProvingEnvironmentforHigherOrderLogic.CambridgeUniversityPress,1993.
B.Guillaume.The se-calculusDoesNotPreserveStrongNormalization.JournalofFunctionalPro-gramming,1999.Toappear.
R.Harper,F.Honsell,andG.Plotkin.Aframeworkforde ninglogics.JournaloftheAssociationforComputingMachinery,40(1):143{184,1993.
J.R.Hindley.BasicSimpleTypeTheory.Number42inCambridgeTractsinTheoreticalComputerScience.CambridgeUniversityPress,1997.
G.Huet.AUni cationAlgorithmforTyped -Calculus.TheoreticalComputerScience,1:27{57,1975.
F.KamareddineandA.R os.A -calculus aladeBruijnwithExplicitSubstitutions.InProc.ofPLILP'95,volume982ofLNCS,pages45{62.Springer,1995.
F.KamareddineandA.R os.Extendinga -calculuswithExplicitSubstitutionwhichPreservesStrongNormalisationintoaCon uentCalculusonOpenTerms.JournalofFunctionalProgramming,7:395{420,1997.
F.KamareddineandA.R os.Relatingthe -and s-StylesofExplicitSubstitutions.JournalofLogicandComputation,10(3):349{380,2000.
D.Kesner.Con uencepropertiesofextensionalandnon-extensional -calculiwithexplicitsubstitu-tions(extendedabstract).InH.Ganzinger,editor,ProceedingsoftheSeventhInternationalConfer-enceonRewritingTechniquesandApplications(RTA-96),volume1103ofLNCS,pages184{199,NewBrunswick,NewJersey,1996.Springer-Verlag.
C.KirchnerandC.Ringeissen.Higher-orderEquationalUni cationviaExplicitSubstitutions.InProc.AlgebraicandLogicProgramming,volume1298ofLNCS,pages61{75.Springer,1997
S.C.Kleene. -de nabilityandrecursiveness.DukeMathematicalJournal,2:340{353,1936
P.Lescanne.From to aJourneyThroughCalculiofExplicitSubstitutions.InProceedingsofthe21stAnnualACMSIGPLAN-SIGACTSymposiumonPrinciplesofProgrammingLanguages,pages60{69,January1994.
P.LescanneandJ.Rouyer-Degli.ExplicitsubstitutionswithdeBruijn'slevels.InJ.Hsiang,edi-tor,ProceedingsoftheInternationalConferenceonRewritingTechniquesandApplications(RTA-95),volume914ofLNCS,pages294{308,ChapelHill,NorthCarolina,1995.Springer-Verla
P.-A.Melli es.Typed -calculiwithexplicitsubstitutionsmaynotterminateinProceedingsofTLCA'95.LNCS,902,1995
D.Miller. Prolog:AnIntroductiontotheLanguageanditsLogic.Draft,DepartmentofComputerScienceandEngineering,ThePennsylvaniaStateUniversity,1998.
RobinMilner,M.Tofte,andR.Harper.TheDe nitionofStandardML.MITPress,Cambridge,MA,1991.
C.Mu~noz.Con uenceandpreservationofstrongnormalisationinanexplicitsubstitutionscalculus(extendedabstract).InProceedingsoftheEleventhAnnualIEEESymposiumonLogicinComputerScience,pages440{447,NewBrunswick,NewJersey,July1996.IEEEComputerSocietyPress.19
C.Mu~noz.Aleft-linearvariantof .InProc.InternationalConferencePLILP/ALP/HOA'97,volume1298ofLNCS,pages224{234,Southampton(England),September1997.Springer.
C.Mu~noz.Uncalculdesubstitutionspourlarepr esentationdepreuvespartiellesenth eoriedetypes.PhDthesis,Universit eParis7,1997.EnglishversioninRapportderechercheINRIARR-3309,1997.
C.Mu~noz.Dependenttypesandexplicitsubstitutions.AcceptedforpublicationinthejournalMathe-maticalStructuresinComputerScience.ItalsoappearsasreportNASA/CR-1999-209722ICASENo.99-43.,1999.
C.Mu~noz.Proof-termsynthesisondependent-typesystemsviaexplicitsubstitutions.AcceptedforpublicationinthejournalTheoreticalComputerScience.ItalsoappearsasreportNASA/CR-1999-209730ICASENo.99-47.andwaspresentedintheInternationalWorkshoponExplicitSubstitutions:TheoryandApplicationstoProgramsandProofs-WESTAPP98,Tsukuba,Japan,2000.
G.Nadathur.A ne-grainednotationforlambdatermsanditsuseinintensionaloperations.TechnicalReportTR-96-13,DepartmentofComputerScience,UniversityofChicago,May301996.AcceptedforpublicationinJournalofFunctionalandLogicProgramming.
G.NadathurandD.S.Wilson.ANotationforLambdaTermsAGeneralizationofEnvironments.TheoreticalComputerScience,198:49{98,1998.
R.P.Nederpelt,J.H.Geuvers,andR.C.deVrijer.SelectedpapersonAutomath.North-Holland,Amsterdam,1994.
S.Owre,J.M.Rushby,andN.Shankar.PVS:Aprototypeveri cationsystem.InD.Kapur,editor,11thInternationalConferenceonAutomatedDeduction(CADE),volume607ofLectureNotesinArti cialIntelligence,pages748{752,Saratoga,NY,June1992.Springer-Verlag.
F.PfenningandC.Sch urmann.Twelfuser'sguide,1.2.edition.TechnicalReportCMU-CS-1998-173,CarnegieMellonUniversity,September1998.
C.Prehofer.ProgressinTheoreticalComputerScience.InR.V.Book,editor,SolvingHigher-OrderEquations:FromLogictoProgramming.Birkh auser,1997.
C.Prehofer.ProgressinTheoreticalComputerScience.InR.V.Book,editor,SolvingHigher-OrderEquations:FromLogictoProgramming.Birkh auser,1997.
A.R os.Contributions al' etudede -calculsavecdessubstitutionsexplicites.Th esededoctorat,Universit eParisVII,1993.
J.A.Robinson.AMachine-orientedLogicBasedontheResolutionPrinciple.JournaloftheACM,12(1):23{41,January1965.
K.H.Rose.ExplicitSubstitution-Tutorial&Survey.BRICS,LectureSeriesLS-96-3,DepartmentofComputerScience,UniversityofAarhus,1996.
W.SnyderandJ.Gallier.Higher-OrderUni cationRevisited:CompleteSetsofTransformations.JournalofSymbolicComputation,8:101{140,1989.
A.N.WhiteheadandB.Russell.PrincipiaMathematica.CambridgeUniversityPress,Cambridge,revisededition,1925{1927.Threevolumes.The rsteditionwaspublished1910{1913.20
dc.rights.none.fl_str_mv Derechos de autor 2000 Revista Colombiana de Computación
dc.rights.coar.fl_str_mv http://purl.org/coar/access_right/c_abf2
dc.rights.uri.*.fl_str_mv http://creativecommons.org/licenses/by-nc-sa/4.0/
dc.rights.uri.none.fl_str_mv http://creativecommons.org/licenses/by-nc-nd/2.5/co/
dc.rights.creativecommons.*.fl_str_mv Atribución-NoComercial-SinDerivadas 2.5 Colombia
rights_invalid_str_mv Derechos de autor 2000 Revista Colombiana de Computación
http://creativecommons.org/licenses/by-nc-sa/4.0/
http://creativecommons.org/licenses/by-nc-nd/2.5/co/
Atribución-NoComercial-SinDerivadas 2.5 Colombia
http://purl.org/coar/access_right/c_abf2
dc.format.mimetype.spa.fl_str_mv application/pdf
dc.publisher.none.fl_str_mv Universidad Autónoma de Bucaramanga UNAB
publisher.none.fl_str_mv Universidad Autónoma de Bucaramanga UNAB
dc.source.none.fl_str_mv Revista Colombiana de Computación; Vol. 1 Núm. 1 (2000): Revista Colombiana de Computación; 46-72
institution Universidad Autónoma de Bucaramanga - UNAB
bitstream.url.fl_str_mv https://repository.unab.edu.co/bitstream/20.500.12749/9084/1/Ayala%20Rincon%2c%20Mauricio_Sustituciones%20expl%c3%adcitas%20y%20todo%20eso.pdf
https://repository.unab.edu.co/bitstream/20.500.12749/9084/2/Ayala%20Rincon%2c%20Mauricio_Sustituciones%20expl%c3%adcitas%20y%20todo%20eso.pdf.jpg
bitstream.checksum.fl_str_mv 5d4c61e252d81a08832485ccbbae030b
d22581292316d8defcefecfea5c155fb
bitstream.checksumAlgorithm.fl_str_mv MD5
MD5
repository.name.fl_str_mv Repositorio Institucional | Universidad Autónoma de Bucaramanga - UNAB
repository.mail.fl_str_mv repositorio@unab.edu.co
_version_ 1814277382560808960
spelling Ayala Rincón, Mauriciof681e303-3263-42cb-a9d5-96197d20d516Muñoz, César0657636a-163f-4fc8-8eb9-3e3f83086197Ayala Rincón, Mauricio [hd3UcpsAAAAJ]Ayala Rincón, Mauricio [0000-0003-0089-3905]Ayala Rincón, Mauricio [Mauricio-Ayala-Rincon]2020-10-27T00:21:41Z2020-10-27T00:21:41Z2000-12-012539-21151657-2831http://hdl.handle.net/20.500.12749/9084instname:Universidad Autónoma de Bucaramanga UNABrepourl:https://repository.unab.edu.coLos 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.Explicit 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.application/pdfspaUniversidad Autónoma de Bucaramanga UNABhttps://revistas.unab.edu.co/index.php/rcc/article/view/1128/1098https://revistas.unab.edu.co/index.php/rcc/article/view/1128M.Abadi,L.Cardelli,P.-L.Curien,andJ.-J.L evy.ExplicitSubstitutions.JournalofFunctionalProgramming,1(4):375{416,1991.M.Ayala-Rinc onandF.Kamareddine.Uni cationvia se-StyleofExplicitSubstitution.In2ndInternationalConferenceonPrinciplesandPracticeofDeclarativeProgramming,Montreal,Canada,September2000.ACMPress.H.P.Barendregt.TheLambdaCalculus:ItsSyntaxandSemantics(revisededition).NorthHolland,1984.H.P.Barendregt. -calculiwithtypes.HandbookofLogicinComputerScience,II,1992.B.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.N.Bj rnerandC.Mu~noz.Absoluteexplicituni cation.Acceptedforpublication.Internationalcon-ferenceonRewritingTechniquesandApplications(RTA'2000),July2000.R.Bloo.PreservationofTerminationforExplicitSubstitution.PhDthesis,DepartmentofMathematicsandComputingScience,EindhovenUniversityofTechnology,1997R.BlooandK.H.Rose.Preservationofstrongnormalisationinnamedlambdacalculiwithexplicitsubstitutionandgarbagecollection.InProc.CSN-95:ComputerScienceintheNetherlands,November1995.D.Briaud.Higherorderuni cationasatypednarrowing.Technicalreport,CRINreport96-R-112,1996.A.Church.Anunsolvableproblemofelementarynumbertheory.AmericanJournalofMathematics,58:345{363,1936.A.Church.Aformulationofthesimpletheoryoftypes.JournalofSymbolicLogic,5:56{68,1940.A.Church.TheCalculiofLambda-Conversion.PrincetonUniversityPress,1941.H.CirsteaandC.Kirchner.CombiningHigher-OrderandFirst-OrderComputationUsingp-Calculus:TowardsaSemanticsofELAN.InD.M.GabbayandM.deRijke,editors,FrontiersofCombiningSystems2,StudiesonLogicandComputation,7,chapter6,pages95{121.ResearchStudiesPress/Wiley,1999.H.CirsteaandC.Kirchner.IntroductiontotheRewritingCalculus.RapportdeRecherche3818,INRIA,December1999.T.Coquand.UneTh eoriedeConstructions.Th esededoctorat,U.ParisVII,1985.T.CoquandandG.Huet.TheCalculusofConstructions.InformationandComputation,76:96{120,1988P.-L.Curien,T.Hardin,andJ.-J.L evy.Con uencePropertiesofWeakandStrongCalculiofExplicitSubstitutions.JournaloftheACM,43(2):362{397,1996.AlsoasRapportdeRechercheINRIA1617,1992.H.B.CurryandR.Feys.CombinatoryLogic,volume1.NorthHolland,1958.N.G.deBruijn.Lambda-CalculusNotationwithNamelessDummies,aToolforAutomaticFormulaManipulation,withApplicationtotheChurch-RosserTheorem.Indag.Mat.,34(5):381{392,1972.G.Dowek.Acompleteproofsynthesismethodfortypesystemsofthecube.JournalofLogicandComputation,3(3):287{315,June1993.G.Dowek,T.Hardin,andC.Kirchner.Higher-orderUni cationviaExplicitSubstitutions.InformationandComputation,157(1/2):183{235,2000.G.Dowek,T.Hardin,C.Kirchner,andF.Pfenning.Uni cationviaexplicitsubstitutions:Thecaseofhigher-orderpatterns.InM.Maher,editor,ProceedingsoftheJointInternationalConferenceandSymposiumonLogicProgramming,Bonn,Germany,September1996.MITPress.W.Farmer.AUni cationAlgorithmforSecond-OrderMonadicTerms.AnnalsofPureandAppliedLogic,39:131{174,1988.M.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.JeanYvesGirard.Interpr etationFonctionelleet EliminationdesCompuresdel'Arithm eticd'OrdreSup erieur.Th esededoctorat,Universit eParisVII,1972.W.Goldfarb.TheUndecidabilityoftheSecond-OrderUni cationProblem.TheoreticalComputerScience,13(2):225{230,1981.M.J.C.GordonandT.F.Melham.IntroductiontoHOL:ATheoremProvingEnvironmentforHigherOrderLogic.CambridgeUniversityPress,1993.B.Guillaume.The se-calculusDoesNotPreserveStrongNormalization.JournalofFunctionalPro-gramming,1999.Toappear.R.Harper,F.Honsell,andG.Plotkin.Aframeworkforde ninglogics.JournaloftheAssociationforComputingMachinery,40(1):143{184,1993.J.R.Hindley.BasicSimpleTypeTheory.Number42inCambridgeTractsinTheoreticalComputerScience.CambridgeUniversityPress,1997.G.Huet.AUni cationAlgorithmforTyped -Calculus.TheoreticalComputerScience,1:27{57,1975.F.KamareddineandA.R os.A -calculus aladeBruijnwithExplicitSubstitutions.InProc.ofPLILP'95,volume982ofLNCS,pages45{62.Springer,1995.F.KamareddineandA.R os.Extendinga -calculuswithExplicitSubstitutionwhichPreservesStrongNormalisationintoaCon uentCalculusonOpenTerms.JournalofFunctionalProgramming,7:395{420,1997.F.KamareddineandA.R os.Relatingthe -and s-StylesofExplicitSubstitutions.JournalofLogicandComputation,10(3):349{380,2000.D.Kesner.Con uencepropertiesofextensionalandnon-extensional -calculiwithexplicitsubstitu-tions(extendedabstract).InH.Ganzinger,editor,ProceedingsoftheSeventhInternationalConfer-enceonRewritingTechniquesandApplications(RTA-96),volume1103ofLNCS,pages184{199,NewBrunswick,NewJersey,1996.Springer-Verlag.C.KirchnerandC.Ringeissen.Higher-orderEquationalUni cationviaExplicitSubstitutions.InProc.AlgebraicandLogicProgramming,volume1298ofLNCS,pages61{75.Springer,1997S.C.Kleene. -de nabilityandrecursiveness.DukeMathematicalJournal,2:340{353,1936P.Lescanne.From to aJourneyThroughCalculiofExplicitSubstitutions.InProceedingsofthe21stAnnualACMSIGPLAN-SIGACTSymposiumonPrinciplesofProgrammingLanguages,pages60{69,January1994.P.LescanneandJ.Rouyer-Degli.ExplicitsubstitutionswithdeBruijn'slevels.InJ.Hsiang,edi-tor,ProceedingsoftheInternationalConferenceonRewritingTechniquesandApplications(RTA-95),volume914ofLNCS,pages294{308,ChapelHill,NorthCarolina,1995.Springer-VerlaP.-A.Melli es.Typed -calculiwithexplicitsubstitutionsmaynotterminateinProceedingsofTLCA'95.LNCS,902,1995D.Miller. Prolog:AnIntroductiontotheLanguageanditsLogic.Draft,DepartmentofComputerScienceandEngineering,ThePennsylvaniaStateUniversity,1998.RobinMilner,M.Tofte,andR.Harper.TheDe nitionofStandardML.MITPress,Cambridge,MA,1991.C.Mu~noz.Con uenceandpreservationofstrongnormalisationinanexplicitsubstitutionscalculus(extendedabstract).InProceedingsoftheEleventhAnnualIEEESymposiumonLogicinComputerScience,pages440{447,NewBrunswick,NewJersey,July1996.IEEEComputerSocietyPress.19C.Mu~noz.Aleft-linearvariantof .InProc.InternationalConferencePLILP/ALP/HOA'97,volume1298ofLNCS,pages224{234,Southampton(England),September1997.Springer.C.Mu~noz.Uncalculdesubstitutionspourlarepr esentationdepreuvespartiellesenth eoriedetypes.PhDthesis,Universit eParis7,1997.EnglishversioninRapportderechercheINRIARR-3309,1997.C.Mu~noz.Dependenttypesandexplicitsubstitutions.AcceptedforpublicationinthejournalMathe-maticalStructuresinComputerScience.ItalsoappearsasreportNASA/CR-1999-209722ICASENo.99-43.,1999.C.Mu~noz.Proof-termsynthesisondependent-typesystemsviaexplicitsubstitutions.AcceptedforpublicationinthejournalTheoreticalComputerScience.ItalsoappearsasreportNASA/CR-1999-209730ICASENo.99-47.andwaspresentedintheInternationalWorkshoponExplicitSubstitutions:TheoryandApplicationstoProgramsandProofs-WESTAPP98,Tsukuba,Japan,2000.G.Nadathur.A ne-grainednotationforlambdatermsanditsuseinintensionaloperations.TechnicalReportTR-96-13,DepartmentofComputerScience,UniversityofChicago,May301996.AcceptedforpublicationinJournalofFunctionalandLogicProgramming.G.NadathurandD.S.Wilson.ANotationforLambdaTermsAGeneralizationofEnvironments.TheoreticalComputerScience,198:49{98,1998.R.P.Nederpelt,J.H.Geuvers,andR.C.deVrijer.SelectedpapersonAutomath.North-Holland,Amsterdam,1994.S.Owre,J.M.Rushby,andN.Shankar.PVS:Aprototypeveri cationsystem.InD.Kapur,editor,11thInternationalConferenceonAutomatedDeduction(CADE),volume607ofLectureNotesinArti cialIntelligence,pages748{752,Saratoga,NY,June1992.Springer-Verlag.F.PfenningandC.Sch urmann.Twelfuser'sguide,1.2.edition.TechnicalReportCMU-CS-1998-173,CarnegieMellonUniversity,September1998.C.Prehofer.ProgressinTheoreticalComputerScience.InR.V.Book,editor,SolvingHigher-OrderEquations:FromLogictoProgramming.Birkh auser,1997.C.Prehofer.ProgressinTheoreticalComputerScience.InR.V.Book,editor,SolvingHigher-OrderEquations:FromLogictoProgramming.Birkh auser,1997.A.R os.Contributions al' etudede -calculsavecdessubstitutionsexplicites.Th esededoctorat,Universit eParisVII,1993.J.A.Robinson.AMachine-orientedLogicBasedontheResolutionPrinciple.JournaloftheACM,12(1):23{41,January1965.K.H.Rose.ExplicitSubstitution-Tutorial&Survey.BRICS,LectureSeriesLS-96-3,DepartmentofComputerScience,UniversityofAarhus,1996.W.SnyderandJ.Gallier.Higher-OrderUni cationRevisited:CompleteSetsofTransformations.JournalofSymbolicComputation,8:101{140,1989.A.N.WhiteheadandB.Russell.PrincipiaMathematica.CambridgeUniversityPress,Cambridge,revisededition,1925{1927.Threevolumes.The rsteditionwaspublished1910{1913.20Derechos de autor 2000 Revista Colombiana de Computaciónhttp://creativecommons.org/licenses/by-nc-sa/4.0/http://creativecommons.org/licenses/by-nc-nd/2.5/co/Atribución-NoComercial-SinDerivadas 2.5 Colombiahttp://purl.org/coar/access_right/c_abf2Revista Colombiana de Computación; Vol. 1 Núm. 1 (2000): Revista Colombiana de Computación; 46-72Innovaciones tecnológicasCiencia de los computadoresDesarrollo de tecnologíaIngeniería de sistemasInvestigacionesTecnologías de la información y las comunicacionesTIC´sTechnological innovationsComputer scienceTechnology developmentSystems engineeringInvestigationsInformation and communication technologiesICT'sClean SustituciónOrden superiorTeoría de la reescrituraProgramacionInnovaciones tecnológicasCiencias de la ComputaciónDesarrollo tecnológicoIngeniería de sistemasInvestigacionesSustitución explícitaOrden superiorTeoría de la reescrituraProgramaciónSustituciones explícitas y todo esoExplicit substitions and all thatinfo:eu-repo/semantics/articleArtículohttp://purl.org/coar/resource_type/c_7a1fhttp://purl.org/coar/resource_type/c_2df8fbb1http://purl.org/redcol/resource_type/CJournalArticlehttp://purl.org/coar/version/c_970fb48d4fbd8a85ORIGINALAyala Rincon, Mauricio_Sustituciones explícitas y todo eso.pdfAyala Rincon, Mauricio_Sustituciones explícitas y todo eso.pdfArtículoapplication/pdf368970https://repository.unab.edu.co/bitstream/20.500.12749/9084/1/Ayala%20Rincon%2c%20Mauricio_Sustituciones%20expl%c3%adcitas%20y%20todo%20eso.pdf5d4c61e252d81a08832485ccbbae030bMD51open accessTHUMBNAILAyala Rincon, Mauricio_Sustituciones explícitas y todo eso.pdf.jpgAyala Rincon, Mauricio_Sustituciones explícitas y todo eso.pdf.jpgIM Thumbnailimage/jpeg8913https://repository.unab.edu.co/bitstream/20.500.12749/9084/2/Ayala%20Rincon%2c%20Mauricio_Sustituciones%20expl%c3%adcitas%20y%20todo%20eso.pdf.jpgd22581292316d8defcefecfea5c155fbMD52open access20.500.12749/9084oai:repository.unab.edu.co:20.500.12749/90842022-11-17 21:45:48.873open accessRepositorio Institucional | Universidad Autónoma de Bucaramanga - UNABrepositorio@unab.edu.co

Publicaciones similares