Mnacho Echenim

Documents

Présentation

Publications

	Unbiasing and robustifying implied volatility calibration in a cryptocurrency market with large bid-ask spreads and missing quotes Mnacho Echenim , Emmanuel Gobet , Anne-Claire Maurice Quantitative Finance, 2023, 23 (9), pp.1285-1304. ⟨10.1080/14697688.2023.2229022⟩ Article dans une revue hal-03715921v1
	Entailment is Undecidable for Symbolic Heap Separation Logic Formulae with Non-Established Inductive Rules Mnacho Echenim , Radu Iosif , Nicolas Peltier Information Processing Letters, 2022 Article dans une revue hal-02951859v2
	The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates Mnacho Echenim , Radu Iosif , Nicolas Peltier ACM Transactions on Computational Logic, 2020, 21 Article dans une revue hal-02388326v1
	Formalizing the Cox–Ross–Rubinstein Pricing of European Derivatives in Isabelle/HOL Mnacho Echenim , Hervé Guiol , Nicolas Peltier Journal of Automated Reasoning, 2020, 64 (4), pp.737-765. ⟨10.1007/s10817-019-09528-w⟩ Article dans une revue hal-02990376v1
	Prime Implicate Generation in Equational Logic Mnacho Echenim , Nicolas Peltier , Sophie Tourret Journal of Artificial Intelligence Research, 2017, 60, pp.827-880 Article dans une revue hal-01946538v1
	A Superposition Calculus for Abductive Reasoning Mnacho Echenim , Nicolas Peltier Journal of Automated Reasoning, 2016, 57 (2), pp.97--134 Article dans une revue hal-01363997v1
	Instantiation Schemes for Nested Theories Mnacho Echenim , Nicolas Peltier ACM Transactions on Computational Logic, 2013, 14 (2), pp.11:1-33. ⟨10.1145/2480759.2480763⟩ Article dans une revue hal-00933873v1
	A Resolution Calculus for First-order Schemata Vincent Aravantinos , Mnacho Echenim , Nicolas Peltier Fundamenta Informaticae, 2013, 125 (2), pp.101-133. ⟨10.3233/FI-2013-855⟩ Article dans une revue hal-00933896v1
	An Instantiation Scheme for Satisfiability Modulo Theories Mnacho Echenim , Nicolas Peltier Journal of Automated Reasoning, 2012, 48 (3), pp.293-362. ⟨10.1007/s10817-010-9200-3⟩ Article dans une revue hal-00933247v1
	Modular Instantiation Schemes Mnacho Echenim , Nicolas Peltier Information Processing Letters, 2011, 111 (20), pp.989-993. ⟨10.1016/j.ipl.2011.07.003⟩ Article dans une revue hal-00931264v1
	Theory decision by decomposition Maria Paola Bonacina , Mnacho Echenim Journal of Symbolic Computation, 2010, 45 (2), pp.229-260. ⟨10.1016/j.jsc.2008.10.008⟩ Article dans une revue hal-00940845v1

	Quantitative modelling and analysis of the Automated Market Maker Uniswap Mnacho Echenim , Emmanuel Gobet , Anne-Claire Maurice International Conference on Computational Finance, CWI, Apr 2024, Amsterdam, Netherlands Communication dans un congrès hal-04507022v1
	Mathematical modelling and analysis of Impermanent Loss and Fees in Uniswap v3 Mnacho Echenim , Emmanuel Gobet , Anne-Claire Maurice Financial Risks International Forum, Mar 2024, Paris, France Communication dans un congrès hal-04511393v1
	Mathematical modelling and analysis of Impermanent Loss and Fees in Uniswap v3 Mnacho Echenim , Emmanuel Gobet , Anne-Claire Maurice Blockchain@X-OMI Workshop on Blockchain and Decentralized Finance, Sep 2023, Paris, France Communication dans un congrès hal-04506995v1
	Statistical Error Bounds for Weighted Mean and Median, with Application to Robust Aggregation of Cryptocurrency Data Michaël Allouche , Mnacho Echenim , Emmanuel Gobet , Anne-Claire Maurice Workshop "Stochastics around Finance", Aug 2023, Kanazawa, Japan Communication dans un congrès hal-04506997v1
	A Strict Constrained Superposition Calculus for Graphs Rachid Echahed , Mnacho Echenim , Mehdi Mhalla , Nicolas Peltier FOSSACS 2023: 26th International Conference on Foundations of Software Science and Computation Structures, Apr 2023, Paris, France Communication dans un congrès hal-03978913v2
	Unbiasing and robustifying implied volatility calibration in a cryptocurrency market with large bid-ask spreads and missing quotes Mnacho Echenim , Emmanuel Gobet , Anne-Claire Maurice Research in Options, FGV-IMPA, Aug 2022, Rio de Jaineiro, Brazil Communication dans un congrès hal-04506993v1
	Decidable Entailments in Separation Logic with Inductive Definitions: Beyond Establishment Mnacho Echenim , Radu Iosif , Nicolas Peltier 29th EACSL Annual Conference on Computer Science Logic, Jan 2021, Ljubljana, Slovenia. ⟨10.4230/LIPIcs.CSL.2021.12⟩ Communication dans un congrès hal-03052687v1
	The Lower Bound of Decidable Entailments in Separation Logic with Inductive Definitions Mnacho Echenim , Radu Iosif , Nicolas Peltier ADSL 2020 - Workshop on Automated Deduction in Separation Logic, 2020, New Orleans, United States Communication dans un congrès hal-02388028v1
	Entailment Checking in Separation Logic with Inductive Definitions is 2-EXPTIME hard Mnacho Echenim , Radu Iosif , Nicolas Peltier LPAR 2020, 2020, Alicante, Spain. ⟨10.1145/3380809⟩ Communication dans un congrès hal-02990396v1
	Prenex Separation Logic with One Selector Field Mnacho Echenim , Radu Iosif , Nicolas Peltier Automated Reasoning with Analytic Tableaux and Related Methods - 28th International Conference, 2019, London, United Kingdom. pp.409-427, ⟨10.1007/978-3-030-29026-9_23⟩ Communication dans un congrès hal-02323468v1
	Ilinva: Using Abduction to Generate Loop Invariants Mnacho Echenim , Nicolas Peltier , Yanis Sellami Frontiers of Combining Systems - 12th International Symposium, 2019, London, United Kingdom. pp.77-93, ⟨10.1007/978-3-030-29007-8_5⟩ Communication dans un congrès hal-02323446v1
	The Bernays-Schönfinkel-Ramsey Class of Separation Logic on Arbitrary Domains Mnacho Echenim , Radu Iosif , Nicolas Peltier Foundations of Software Science and Computation Structures (FOSSACS) - 22nd International Conference, 2019, Prague, Czech Republic. pp.242-259, ⟨10.1007/978-3-030-17127-8_14⟩ Communication dans un congrès hal-02094154v1
	A Generic Framework for Implicate Generation Modulo Theories Mnacho Echenim , Nicolas Peltier , Yanis Sellami IJCAR, Jul 2018, Oxford, United Kingdom Communication dans un congrès hal-01833514v1
	Prime Implicate Generation in Equational Logic Mnacho Echenim , Nicolas Peltier , Sophie Tourret Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018, 2018, Stockholm, Sweden Communication dans un congrès hal-01946497v1
	The Binomial Pricing Model in Finance: A Formalization in Isabelle Nicolas Peltier , Mnacho Echenim CADE 26, 2017, Gothenburg, Sweden. pp.546-562 Communication dans un congrès hal-01562944v1
	Quantifier-Free Equational Logic and Prime Implicate Generation Mnacho Echenim , Nicolas Peltier , Sophie Tourret CADE-25, Jul 2015, Berlin, Germany. pp.311-325, ⟨10.1007/978-3-319-21401-6_21⟩ Communication dans un congrès hal-01363987v1
	A Superposition-Based Approach to Abductive Reasoning in Equational Clausal Logic Mnacho Echenim , Nicolas Peltier , Sophie Tourret ADDTC 2014, Jul 2014, Vienna, Austria Communication dans un congrès hal-01132800v1
	A Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses Mnacho Echenim , Nicolas Peltier , Sophie Tourret PAAR 2014, Jul 2014, Vienna, Austria Communication dans un congrès hal-01132801v1
	A Rewriting Strategy to Generate Prime Implicates in Equational Logic Mnacho Echenim , Nicolas Peltier , Sophie Tourret IJCAR 2014, Jul 2014, Vienna, Austria. pp.137-151 Communication dans un congrès hal-01018692v1
	An Approach to Abductive Reasoning in Equational Logic Mnacho Echenim , Nicolas Peltier , Sophie Tourret IJCAI 2013 - International Joint Conference on Artificial Intelligence, Aug 2013, Beijing, China. pp.531-537 Communication dans un congrès hal-00934278v1
	A Calculus for Generating Ground Explanations Mnacho Echenim , Nicolas Peltier IJCAR 2012 - International Joint Conference on Automated Reasoning, Jun 2012, Manchester, United Kingdom. pp.194-209, ⟨10.1007/978-3-642-31365-3_17⟩ Communication dans un congrès hal-00933272v1
	Reasoning on Schemata of Formulæ Mnacho Echenim , Nicolas Peltier AISC 2012 - Artificial Intelligence and Symbolic Computation (Part of CICM 2012), Jul 2012, Bremen, Germany. pp.310-325, ⟨10.1007/978-3-642-31374-5_21⟩ Communication dans un congrès hal-00933516v1
	A Superposition Strategy for Abductive Reasoning in Ground Equational Logic Mnacho Echenim , Nicolas Peltier , Sophie Tourret IWS 2012 - International Workshop on Strategies in Rewriting, Proving and Programming (IJCAR 2012 workshop ), Jul 2012, Manchester, United Kingdom. pp.4-11 Communication dans un congrès hal-00933582v1
	Instantiation of SMT Problems Modulo Integers Mnacho Echenim , Nicolas Peltier International Conference on Artificial Intelligence and Symbolic Computation, 2010, Paris, France. pp.49-63, ⟨10.1007/978-3-642-14128-7_6⟩ Communication dans un congrès hal-00940668v1

	Pricing in discrete financial models Mnacho Echenim 2018 Autre publication scientifique hal-01959544v1

	Statistical error bounds for weighted mean and median, with application to robust aggregation of cryptocurrency data Michaël Allouche , Mnacho Echenim , Emmanuel Gobet , Anne-Claire Maurice 2023 Pré-publication, Document de travail hal-04017151v1
	Thorough mathematical modelling and analysis of Uniswap v3 Mnacho Echenim , Emmanuel Gobet , Anne-Claire Maurice 2023 Pré-publication, Document de travail hal-04214315v2
	On the Expressive Completeness of Bernays-Sch\"onfinkel-Ramsey Separation Logic Mnacho Echenim , Radu Iosif , Nicolas Peltier 2018 Pré-publication, Document de travail hal-01699151v1
	The Complexity of Prenex Separation Logic with One Selector Mnacho Echenim , Radu Iosif , Nicolas Peltier 2018 Pré-publication, Document de travail hal-01946528v1
	Solving Linear Constraints in Elementary Abelian p-Groups of Symmetries Thierry Boy de La Tour , Mnacho Echenim 2011 Pré-publication, Document de travail hal-00940852v1
	Instantiation of SMT problems modulo Integers Mnacho Echenim , Nicolas Peltier 2010 Pré-publication, Document de travail hal-00940677v1

	Checking Entailment Between Separation Logic Symbolic Heaps: Beyond Connected and Established Systems Nicolas Peltier , Radu Iosif , Mnacho Echenim [Research Report] VERIMAG/LIG/CNRS. 2020 Rapport hal-03088890v1
	A Calculus for Generating Ground Explanations (Technical Report) Mnacho Echenim , Nicolas Peltier 2012 Rapport hal-00933750v1
	A Resolution Calculus for First-Order Schemata Vincent Aravantinos , Mnacho Echenim , Nicolas Peltier 2011 Rapport hal-00932856v1
	A Resolution Calculus for Propositional Schemata Vincent Aravantinos , Mnacho Echenim , Nicolas Peltier 2011 Rapport hal-00932855v1

	Déduction et Unification dans les Théories Permutatives Mnacho Echenim Autre [cs.OH]. Institut National Polytechnique de Grenoble - INPG, 2005. Français. ⟨NNT : ⟩ Thèse tel-00011236v1

Mnacho Echenim

Présentation

Publications

Unbiasing and robustifying implied volatility calibration in a cryptocurrency market with large bid-ask spreads and missing quotes

Entailment is Undecidable for Symbolic Heap Separation Logic Formulae with Non-Established Inductive Rules

The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates

Formalizing the Cox–Ross–Rubinstein Pricing of European Derivatives in Isabelle/HOL

Prime Implicate Generation in Equational Logic

A Superposition Calculus for Abductive Reasoning

Instantiation Schemes for Nested Theories

A Resolution Calculus for First-order Schemata

An Instantiation Scheme for Satisfiability Modulo Theories

Modular Instantiation Schemes

Theory decision by decomposition

Quantitative modelling and analysis of the Automated Market Maker Uniswap

Mathematical modelling and analysis of Impermanent Loss and Fees in Uniswap v3

Mathematical modelling and analysis of Impermanent Loss and Fees in Uniswap v3

Statistical Error Bounds for Weighted Mean and Median, with Application to Robust Aggregation of Cryptocurrency Data

A Strict Constrained Superposition Calculus for Graphs

Unbiasing and robustifying implied volatility calibration in a cryptocurrency market with large bid-ask spreads and missing quotes

Decidable Entailments in Separation Logic with Inductive Definitions: Beyond Establishment

The Lower Bound of Decidable Entailments in Separation Logic with Inductive Definitions

Entailment Checking in Separation Logic with Inductive Definitions is 2-EXPTIME hard

Prenex Separation Logic with One Selector Field

Ilinva: Using Abduction to Generate Loop Invariants

The Bernays-Schönfinkel-Ramsey Class of Separation Logic on Arbitrary Domains

A Generic Framework for Implicate Generation Modulo Theories

Prime Implicate Generation in Equational Logic

The Binomial Pricing Model in Finance: A Formalization in Isabelle

Quantifier-Free Equational Logic and Prime Implicate Generation

A Superposition-Based Approach to Abductive Reasoning in Equational Clausal Logic

A Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses

A Rewriting Strategy to Generate Prime Implicates in Equational Logic

An Approach to Abductive Reasoning in Equational Logic

A Calculus for Generating Ground Explanations

Reasoning on Schemata of Formulæ

A Superposition Strategy for Abductive Reasoning in Ground Equational Logic

Instantiation of SMT Problems Modulo Integers

Pricing in discrete financial models

Statistical error bounds for weighted mean and median, with application to robust aggregation of cryptocurrency data

Thorough mathematical modelling and analysis of Uniswap v3

On the Expressive Completeness of Bernays-Sch\"onfinkel-Ramsey Separation Logic

The Complexity of Prenex Separation Logic with One Selector

Solving Linear Constraints in Elementary Abelian p-Groups of Symmetries

Instantiation of SMT problems modulo Integers

Checking Entailment Between Separation Logic Symbolic Heaps: Beyond Connected and Established Systems

A Calculus for Generating Ground Explanations (Technical Report)

A Resolution Calculus for First-Order Schemata

A Resolution Calculus for Propositional Schemata

Déduction et Unification dans les Théories Permutatives