Publications

Export 11 results:
Author Title Type [ Year(Asc)]
Submitted
G. Cano, Cohen, C. , Dénès, M. , Mörtberg, A. , and Siles, V. , Formalized Linear Algebra over Elementary Divisor Rings in Coq, Logical Methods in Computer Science, Submitted.
C. Hritcu, Lampropoulos, L. , Spector-Zabusky, A. , de Amorim, A. Azevedo, Dénès, M. , Hughes, J. , Pierce, B. C. , and Vytiniotis, D. , Testing Noninterference, Quickly, Journal of Functional Programming, no. Special Issue for ICFP 2013, Submitted.
2015
Z. Paraskevopoulou, Hritcu, C. , Dénès, M. , Lampropoulos, L. , and Pierce, B. C. , Foundational Property-Based Testing, in 6th conference on Interactive Theorem Proving, ITP 2015, 2015.
A. Azevedo de Amorim, Dénès, M. , Giannarakis, N. , Hritcu, C. , Pierce, B. C. , Spector-Zabusky, A. , and Tolmach, A. , Micro-Policies: A Framework for Verified, Tag-Based Security Monitors, in 36th IEEE Symposium on Security and Privacy, 2015.
2013
G. Cano and Dénès, M. , Matrices à blocs et en forme canonique, in JFLA - Journées francophones des langages applicatifs, Aussois, France, 2013.
C. Cohen, Dénès, M. , and Mörtberg, A. , Refinements for Free!, in Certified Programs and Proofs - Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings, 2013.
2012
M. Dénès, Mörtberg, A. , and Siles, V. , A refinement-based approach to computational algebra in COQ, in ITP - 3rd International Conference on Interactive Theorem Proving - 2012, Princeton, États-Unis, 2012, vol. 7406, pp. 83-98.
J. Heras, Dénès, M. , Mata, G. , Mörtberg, A. , Poza, M. , and Siles, V. , Towards a certified computation of homology groups for digital images, in CTIC - Computational Topology in Image Context - 2012, Bertinoro, Italie, 2012, vol. 7309, pp. 49-57.
2011
M. Boespflug, Dénès, M. , and Grégoire, B. , Full reduction at full throttle, in Certified Programs and Proofs, 2011.
J. Heras, Poza, M. , Dénès, M. , and Rideau, L. , Incidence simplicial matrices formalized in Coq/SSReflect, in Calculemus, 2011.
2009
M. Dénès, Lesage, B. , Bertot, Y. , and Richard, A. , Formal proof of theorems on genetic regulatory networks, in SYNASC'09, Timisoara, Roumanie, 2009.