Ynot: dependent types for imperative programs Export

@inproceedings{nanevski:ydtfip, abstract = {We describe an axiomatic extension to the Coq proof assistant, that supports writing, reasoning about, and extracting higher-order, dependently-typed programs with side-effects . Coq already includes a powerful functional language that supports dependent types, but that language is limited to pure, total functions. The key contribution of our extension, which we call Ynot, is the added support for computations that may have effects such as non-termination, accessing a mutable store, and throwing/catching exceptions.}, address = {New York, NY, USA}, author = {Nanevski, Aleksandar and Morrisett, Greg and Shinnar, Avraham and Govereau, Paul and Birkedal, Lars}, booktitle = {ICFP '08: Proceeding of the 13th ACM SIGPLAN international conference on Functional programming}, citeulike-article-id = {3390918}, citeulike-linkout-0 = {http://portal.acm.org/citation.cfm?id=1411204.1411237}, citeulike-linkout-1 = {http://dx.doi.org/10.1145/1411204.1411237}, doi = {10.1145/1411204.1411237}, isbn = {978-1-59593-919-7}, keywords = {coq, dependent-types, functional-programming, logic, type-theory}, location = {Victoria, BC, Canada}, pages = {229--240}, posted-at = {2008-11-15 15:16:10}, priority = {2}, publisher = {ACM}, title = {Ynot: dependent types for imperative programs}, url = {http://dx.doi.org/10.1145/1411204.1411237}, year = {2008} }

TY - CONF ID - nanevski:ydtfip L3 - citeulike-article-id:3390918 N2 - We describe an axiomatic extension to the Coq proof assistant, that supports writing, reasoning about, and extracting higher-order, dependently-typed programs with side-effects . Coq already includes a powerful functional language that supports dependent types, but that language is limited to pure, total functions. The key contribution of our extension, which we call Ynot, is the added support for computations that may have effects such as non-termination, accessing a mutable store, and throwing/catching exceptions. CY - Victoria, BC, Canada SN - 978-1-59593-919-7 AD - New York, NY, USA EP - 240 TI - Ynot: dependent types for imperative programs PB - ACM T2 - ICFP '08: Proceeding of the 13th ACM SIGPLAN international conference on Functional programming SP - 229 KW - coq KW - dependent-types KW - functional-programming KW - logic KW - type-theory AU - Nanevski, Aleksandar AU - Morrisett, Greg AU - Shinnar, Avraham AU - Govereau, Paul AU - Birkedal, Lars PY - 2008/// UR - http://dx.doi.org/10.1145/1411204.1411237 ER -