, Plus x y) = (eval env x)`plus`(eval env y) 18 eval env (Sub x y) = (eval env x)`minus`(eval env y) 19 eval env (Mul x y) = (eval env x)`mult`(eval env y) 20 eval env (Div x y) = assert_total $ (eval env x)`div`(eval env y) 21 eval env, False 10 11 eval : (env : Env) -> (e : NumericExpression) -> Nat env

, Xc specification ver. 1.0 (x5965a, 2011.

E. Albert, P. Arenas, G. Puebla, and M. V. Hermenegildo, Certificate size reduction in abstraction-carrying code, TPLP, vol.12, issue.3, pp.283-318, 2012.

A. Andrei, P. Eles, O. Jovanovic, M. T. Schmitz, J. Ogniewski et al., Quasistatic voltage scaling for energy minimization with time constraints, IEEE Trans. VLSI Syst, vol.19, issue.1, pp.10-23, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00181654

D. E. Bell and L. J. La-padula, Secure computer system: Unified exposition and multics interpretation, pp.1-133, 1976.

E. C. Brady, Idris -: Systems programming meets full dependent types, Proceedings of the 5th ACM Workshop on Programming Languages Meets Program Verification, pp.43-54, 2011.

H. Chen, A. Tiu, Z. Xu, and Y. Liu, A permission-dependent type system for secure information flow analysis, CSF, pp.218-232, 2018.

W. Chin and S. Khoo, Calculating sized types, Higher-Order and Symbolic Computation, vol.14, issue.2-3, pp.261-300, 2001.

E. Çiçek, D. Garg, and U. A. Acar, Refinement types for incremental computational complexity, Held as Part of the European Joint Conferences on Theory and Practice of Software, pp.406-431, 2015.

D. D. Clark and D. R. Wilson, A comparison of commercial and military computer security policies, 1987 IEEE Symposium on Security and Privacy, pp.184-184, 1987.

P. Cousot and R. Cousot, Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints, Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, pp.238-252, 1977.

H. David, E. Gorbatov, U. R. Hanebutte, R. Khanna, and C. Le, Rapl: Memory power estimation and capping, Proceedings of the 16th ACM/IEEE International Symposium on Low Power Electronics and Design, pp.189-194, 2010.

M. Di-pirro, M. Conti, and R. Lazzeretti, Ensuring information security by using haskell's advanced type system, 2017 International Carnahan Conference on Security Technology (ICCST), pp.1-6, 2017.

H. Falk and P. Lokuciejewski, A compiler framework for the reduction of worst-case execution times, Real-Time Systems, vol.46, issue.2, pp.251-300, 2010.

R. Focardi and F. Martinelli, A uniform approach for the definition of security properties, FM'99 -Formal Methods, pp.794-813, 1999.

K. Georgiou, S. Kerrison, Z. Chamski, and K. Eder, Energy transparency for deeply embedded programs, TACO, vol.14, issue.1, pp.1-8, 2017.

J. A. Goguen and J. Meseguer, Security policies and security models, 1982 IEEE Symposium on Security and Privacy, pp.11-11, 1982.

J. Gosling, B. Joy, G. L. Steele, G. Bracha, and A. Buckley, The Java Language Specification, 2014.

S. Gulwani, K. K. Mehra, and T. M. Chilimbi, SPEED: precise and efficient static estimation of program computational complexity, Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.127-139, 2009.

M. V. Hermenegildo, G. Puebla, F. Bueno, and P. López-garcía, Integrated program debugging, verification, and optimization using abstract interpretation (and the ciao system preprocessor), Sci. Comput. Program, vol.58, issue.1-2, pp.115-140, 2005.

J. Hoffmann, K. Aehlig, and M. Hofmann, Multivariate amortized resource analysis, ACM Trans. Program. Lang. Syst, vol.34, issue.3, p.62, 2012.

J. Hughes and L. Pareto, Recursion and dynamic data-structures in bounded space: Towards embedded ML programming, Proceedings of the fourth ACM SIGPLAN International Conference on Functional Programming (ICFP '99), pp.70-81, 1999.

G. Hutton, Programming in Haskell, 2007.

M. Joye and S. M. Yen, The montgomery powering ladder, Cryptographic Hardware and Embedded Systems -CHES 2002, pp.291-302, 2003.

D. Kästner, M. Pister, S. Wegener, and C. Ferdinand, TimeWeaver: A Tool for Hybrid Worst-Case Execution Time Analysis, 19th International Workshop on Worst-Case Execution Time Analysis, vol.72, 2019.

S. Kerrison and K. Eder, Energy modeling of software for a hardware multithreaded embedded microprocessor, ACM Trans. Embedded Comput. Syst, vol.14, issue.3, p.25, 2015.

P. Kocher, J. Jaffe, and B. Jun, Differential power analysis, Advances in Cryptology -CRYPTO' 99, pp.388-397, 1999.

P. C. Kocher, Timing attacks on implementations of diffie-hellman, rsa, dss, and other systems, Advances in Cryptology -CRYPTO '96, pp.104-113, 1996.

R. Kumar, A. Rensink, and M. Stoelinga, Locks: A property specification language for security goals, Proceedings of the 33rd Annual ACM Symposium on Applied Computing, pp.1907-1915, 2018.

U. D. Lago and B. Petit, The geometry of types, The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13, pp.167-178, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00909318

Y. S. Li and S. Malik, Performance analysis of embedded software using implicit path enumeration, IEEE Trans. on CAD of Integrated Circuits and Systems, vol.16, issue.12, pp.1477-1487, 1997.

U. Liqat, S. Kerrison, A. Serrano, K. Georgiou, P. López-garcía et al., Energy consumption analysis of programs based on XMOS isa-level models, In: LOPSTR. Lecture Notes in Computer Science, vol.8901, pp.72-90, 2013.

P. López-garcía, L. Darmawan, M. Klemen, U. Liqat, F. Bueno et al., Interval-based resource usage verification by translation into horn clauses and an application to energy consumption, TPLP, vol.18, issue.2, pp.167-223, 2018.

J. Morse, S. Kerrison, and K. Eder, On the limitations of analysing worst-case dynamic energy of processing, ACM Transactions on Embedded Computing Systems, vol.17, issue.3, 2018.

G. C. Necula, Proof-carrying code, Conference Record of POPL'97: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.106-119, 1997.

J. L. Núñez-yáñez and G. Lore, Enabling accurate modeling of power and energy consumption in an arm-based system-on-chip. Microprocessors and Microsystems -Embedded Hardware Design, vol.37, pp.319-332, 2013.

J. Pallister, S. J. Hollis, and J. Bennett, BEEBS: open benchmarks for energy measurements on embedded platforms, 2013.

O. Reparaz, J. Balasch, and I. Verbauwhede, Dude, is my code constant time? In: Design, Automation Test in Europe Conference Exhibition, pp.1697-1702, 2017.

R. L. Rivest, A. Shamir, and L. Adleman, A method for obtaining digital signatures and public-key cryptosystems, Communications of the ACM, vol.21, issue.2, pp.120-126, 1978.

P. Y. Ryan, Mathematical models of computer security, International School on Foundations of Security Analysis and Design, pp.1-62, 2000.

A. Serrano, P. López-garcía, and M. V. Hermenegildo, Resource usage analysis of logic programs via abstract interpretation using sized types, TPLP, vol.14, pp.739-754, 2014.

Y. S. Shao and D. M. Brooks, Energy characterization and instruction-level energy model of intel's xeon phi processor, pp.389-394, 2013.

F. Slama, Automatic generation of proof terms in dependently typed programming languages, 2018.

F. Slama and E. Brady, Automatically proving equivalence by type-safe reflection, Intelligent Computer Mathematics -10th International Conference, CICM 2017, pp.40-55, 2017.

N. Swamy, B. J. Corcoran, and M. Hicks, Fable: A language for enforcing user-defined security policies, 2008 IEEE Symposium on Security and Privacy, pp.369-383, 2008.

V. Tiwari, S. Malik, and A. Wolfe, Power analysis of embedded software: a first step towards software power minimization, IEEE Trans. VLSI Syst, vol.2, issue.4, pp.437-445, 1994.

P. B. Vasconcelos and K. Hammond, Inferring cost equations for recursive, polymorphic and higher-order functional programs, Implementation of Functional Languages, 15th International Workshop, pp.86-101, 2003.

D. M. Volpano, C. E. Irvine, and G. Smith, A sound type system for secure flow analysis, Journal of Computer Security, vol.4, issue.2/3, pp.167-188, 1996.

R. Wilhelm, J. Engblom, A. Ermedahl, N. Holsti, S. Thesing et al., The worst-case execution-time prob-lem—overview of methods and survey of tools, ACM Trans. Embed. Comput. Syst, vol.7, issue.3, pp.1-36, 2008.

R. Wilhelm, J. Engblom, A. Ermedahl, N. Holsti, S. Thesing et al., The Worst-case Execution-time Prob-lem&Mdash;Overview of Methods and Survey of Tools, ACM Trans. Embed. Comput. Syst, vol.7, issue.3, pp.1-36, 2008.

C. Xian, Y. Lu, and Z. Li, Energy-aware scheduling for real-time multiprocessor systems with uncertain task execution time, DAC, pp.664-669, 2007.

H. Ziade, R. Ayoubi, and R. Velazco, A survey on fault injection techniques, International Arab Journal of Information Technology, vol.1, issue.2, pp.171-186, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00105562