Formalization of Programs with Positive Inductive Types

Proof assistants are computer systems that allows a user to do mathematics on a computer helping with the development of formal proof by human-machine collaboration, however most of them only work with strictly positive types, this restriction limits the number of problem that can be formalized. Thi...

Full description

Autores:
Lobo Vesga, Elisabet
Tipo de recurso:
Fecha de publicación:
2014
Institución:
Universidad EAFIT
Repositorio:
Repositorio EAFIT
Idioma:
eng
OAI Identifier:
oai:repository.eafit.edu.co:10784/4552
Acceso en línea:
http://hdl.handle.net/10784/4552
Palabra clave:
Inductive Types
Positive Types
Programming Logic
Continuations
Rights
License
Acceso abierto
id REPOEAFIT2_84ebcfd7737c8642980b72052391418a
oai_identifier_str oai:repository.eafit.edu.co:10784/4552
network_acronym_str REPOEAFIT2
network_name_str Repositorio EAFIT
repository_id_str
spelling 2014-12-10T21:09:38Z2014-112014-12-10T21:09:38Zhttp://hdl.handle.net/10784/4552Proof assistants are computer systems that allows a user to do mathematics on a computer helping with the development of formal proof by human-machine collaboration, however most of them only work with strictly positive types, this restriction limits the number of problem that can be formalized. This is perhaps the reason why verification of programs that use positive (and negative) types is uncommon. Hence, we use the programming logic created by Bove, Dybjer and Sicard- Ram´ırez that accept positive types to formalize the termination of a breadth-first search in a binary tree using continuations data type which is positive.engUniversidad EAFIT, Medellín, ColombiaGrupo de Investigación Lógica y ComputaciónUniversidad EAFIT. Escuela de Ciencias y Humanidades. Grupo de Investigación Lógica y ComputaciónFormalization of Programs with Positive Inductive Typesinfo:eu-repo/semantics/workingPaperworkingPaperDocumento de trabajo de investigacióndrafthttp://purl.org/coar/version/c_b1a7d7d4d402bccehttp://purl.org/coar/resource_type/c_8042Acceso abiertohttp://purl.org/coar/access_right/c_abf2Inductive TypesPositive TypesProgramming LogicContinuationsElizabet Lobo-Vesga (elobove@eafit.edu.co)Lobo Vesga, Elisabetd11984c5-c643-4163-a84f-0646c594531b-1LICENSElicense.txtlicense.txttext/plain; charset=utf-82556https://repository.eafit.edu.co/bitstreams/8dd290f2-918b-498e-abe3-9bd4880a0ecc/download76025f86b095439b7ac65b367055d40cMD51ORIGINALLoboVesga-2014_Practica-investigativa-III_Formalization-of-programs-with-positive-inductive-types.pdfLoboVesga-2014_Practica-investigativa-III_Formalization-of-programs-with-positive-inductive-types.pdfapplication/pdf173135https://repository.eafit.edu.co/bitstreams/a677dff9-b0f0-482b-a00f-510fb2ba63a3/download81432bcce7f31de6d75f8a1ddc44446bMD5210784/4552oai:repository.eafit.edu.co:10784/45522024-12-04 11:49:44.931open.accesshttps://repository.eafit.edu.coRepositorio Institucional Universidad EAFITrepositorio@eafit.edu.co
dc.title.spa.fl_str_mv Formalization of Programs with Positive Inductive Types
title Formalization of Programs with Positive Inductive Types
spellingShingle Formalization of Programs with Positive Inductive Types
Inductive Types
Positive Types
Programming Logic
Continuations
title_short Formalization of Programs with Positive Inductive Types
title_full Formalization of Programs with Positive Inductive Types
title_fullStr Formalization of Programs with Positive Inductive Types
title_full_unstemmed Formalization of Programs with Positive Inductive Types
title_sort Formalization of Programs with Positive Inductive Types
dc.creator.fl_str_mv Lobo Vesga, Elisabet
dc.contributor.eafitauthor.spa.fl_str_mv Elizabet Lobo-Vesga (elobove@eafit.edu.co)
dc.contributor.author.none.fl_str_mv Lobo Vesga, Elisabet
dc.subject.keyword.spa.fl_str_mv Inductive Types
Positive Types
Programming Logic
Continuations
topic Inductive Types
Positive Types
Programming Logic
Continuations
description Proof assistants are computer systems that allows a user to do mathematics on a computer helping with the development of formal proof by human-machine collaboration, however most of them only work with strictly positive types, this restriction limits the number of problem that can be formalized. This is perhaps the reason why verification of programs that use positive (and negative) types is uncommon. Hence, we use the programming logic created by Bove, Dybjer and Sicard- Ram´ırez that accept positive types to formalize the termination of a breadth-first search in a binary tree using continuations data type which is positive.
publishDate 2014
dc.date.available.none.fl_str_mv 2014-12-10T21:09:38Z
dc.date.issued.none.fl_str_mv 2014-11
dc.date.accessioned.none.fl_str_mv 2014-12-10T21:09:38Z
dc.type.none.fl_str_mv info:eu-repo/semantics/workingPaper
dc.type.eng.fl_str_mv workingPaper
dc.type.coarversion.fl_str_mv http://purl.org/coar/version/c_b1a7d7d4d402bcce
dc.type.coar.fl_str_mv http://purl.org/coar/resource_type/c_8042
dc.type.local.spa.fl_str_mv Documento de trabajo de investigación
dc.type.hasVersion.spa.fl_str_mv draft
dc.identifier.uri.none.fl_str_mv http://hdl.handle.net/10784/4552
url http://hdl.handle.net/10784/4552
dc.language.iso.eng.fl_str_mv eng
language eng
dc.rights.coar.fl_str_mv http://purl.org/coar/access_right/c_abf2
dc.rights.local.spa.fl_str_mv Acceso abierto
rights_invalid_str_mv Acceso abierto
http://purl.org/coar/access_right/c_abf2
dc.publisher.spa.fl_str_mv Universidad EAFIT, Medellín, Colombia
dc.publisher.program.spa.fl_str_mv Grupo de Investigación Lógica y Computación
dc.publisher.department.spa.fl_str_mv Universidad EAFIT. Escuela de Ciencias y Humanidades. Grupo de Investigación Lógica y Computación
institution Universidad EAFIT
bitstream.url.fl_str_mv https://repository.eafit.edu.co/bitstreams/8dd290f2-918b-498e-abe3-9bd4880a0ecc/download
https://repository.eafit.edu.co/bitstreams/a677dff9-b0f0-482b-a00f-510fb2ba63a3/download
bitstream.checksum.fl_str_mv 76025f86b095439b7ac65b367055d40c
81432bcce7f31de6d75f8a1ddc44446b
bitstream.checksumAlgorithm.fl_str_mv MD5
MD5
repository.name.fl_str_mv Repositorio Institucional Universidad EAFIT
repository.mail.fl_str_mv repositorio@eafit.edu.co
_version_ 1818102427240366080

Publicaciones similares