1998-2021 Publications

• 2021
  • Th. Hardin, M. Jaume, F. Pessaux, V. Viguie Donzeau‑Gouge : “Concepts and Semantics of Programming Languages 2: Modular and Object‐oriented Constructs with OCaml, Python, C++, Ada and Java”, (ISTE Wiley), (ISBN: Print ISBN:9781786306029 |Online ISBN:9781119851196) (2021)
  • Th. Hardin, M. Jaume, F. Pessaux, V. Viguie Donzeau‑Gouge : “Concepts and Semantics of Programming Languages 1: A Semantical Approach with OCaml and Python”, (ISTE Wiley), (ISBN: Print ISBN:9781786305305 |Online ISBN:9781119824121) (2021)
  • Th. Hardin, M. Jaume, F. Pessaux, V. Viguie Donzeau‑Gouge : “Concepts et sémantique des langages de programmation 1 : constructions fonctionnelles et impératives avec OCaml, Python, C et C++”, (ISTE Editions), (ISBN: 9781784057015) (2021)
  • Th. Hardin, M. Jaume, F. Pessaux, V. Viguie Donzeau‑Gouge : “Concepts et sémantique des langages de programmation 2 : constructions modulaires et objet avec OCaml, Python, C++, Ada et Java”, (ISTE Editions), (ISBN: 9781784057022) (2021)
• 2009
  • É. Jaeger, Th. Hardin : “Yet Another Deep Embedding of B:Extending de Bruijn Notations”, (2009)
  • Ph. Ayrault, Th. Hardin, F. Pessaux : “Development of a Generic Voter under FoCal”, Proceedings of the 3^rd International Conference on Tests and Proofs, vol. 5668, Lecture Notes in Computer Science, Zurich, Switzerland, pp. 10-26, (Springer) (2009)
  • Ph. Ayrault, Th. Hardin, F. Pessaux : “Development life cycle of critical software under FoCal”, Electronic Notes in Theoretical Computer Science, vol. 243, pp. 15-31, (Elsevier) (2009)
• 2008
  • É. Jaeger, Th. Hardin : “A Few Remarks About Formal Development of Secure Systems”, High Assurance Systems Engineering Symposium, 2008. HASE 2008. 11^th IEEE, Nanjing, China, pp. 165-174, (IEEE) (2008)
  • Ph. Ayrault, M. Carlier, D. Delahaye, C. Dubois, D. Doligez, L. Habib, Th. Hardin, M. Jaume, Ch. Morisset, F. Pessaux, R. Rioboo, P. Weis : “Trusted Software within Focal”, Trusting Trusted Computing ?, Rennes, France, pp. 162-179 (2008)
• 2007
  • F. Blanqui, Th. Hardin, P. Weis : “On the implementation of construction functions for non-free concrete data types”, 16^th European Symposium on Programming - ESOP'07, vol. 4421, Lecture Notes in Computer Science, Braga, Portugal, pp. 95-109, (Springer) (2007)
• 2006
  • Th. Hardin : “Modulogic: Présentation d’un modèle de contrôle d’accès et bilan des travaux réalisés”, Journées PaRISTIC 2006, Nancy, France (2006)
  • Th. Hardin, M. Jaume, Ch. Morisset : “Access control and Rewrite Systems”, 1^st International Workshop on Security and Rewriting Techniques, SecReT'06, Venice, Italy, pp. 2-17 (2006)
  • Th. Hardin : “Focal: un atelier de construction modulaire de logiciels, tentant de répondre aux besoins de la sûreté et de la sécurité”, AFADL 2006 Proceedings, Paris, France, pp. 2-3 (2006)
  • Th. Hardin : “Focal: a formally-based IDE and a mathematical framework”, School of Science, Beihang University, Beijing, China (2006)
  • Th. Hardin : “Focal: un atelier de construction modulaire de logiciels, fondé sur lísomorphisme de Curry-Howard”, Séminaire du LIST, CEA, Sacaly, France (2006)
• 2005
  • Th. Hardin : “Modulogic: Présentation des travaux réalisés autour de FOCAL”, Journées PaRISTIC 2005, Bordeaux, France (2005)
• 2004
  • C. Dubois, Th. Hardin, V. Viguie Donzeau‑Gouge : “Building certified components within FOCAL”, TFP 2004 - 5^th Symposium on Trends in Functional Programming, vol. 5, Trends in Functional Programming, Munich, Germany, pp. 33-48, (Intellect) (2004)
  • Th. Hardin : “Modulogic: un atelier de construction modulaire de logiciels certifiés. Application aux politiques de sécurité”, Journées des ACI Sécurité, Toulouse, France (2004)
  • Th. Hardin, R. Rioboo : “Les Objets des Mathématiques”, Revue des Sciences et Technologies de l'Information - Série L'Objet : logiciel, bases de données, réseaux, vol. 10 (4), pp. 83-118, (Hermès-Lavoisier) (2004)
• 2003
  • E. Gureghian, Th. Hardin, M. Jaume : “A full formalisation of the Bell and La Padula security model”, (2003)
  • Th. Hardin, R. Rioboo : “CALCULEMUS-2003 - 11^th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, September 10-12 2003, Roma, Italy”, CALCULEMUS-2003 - 11^th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning n°lip6.2003.010, Rome, Italy, (LIP6) (2003)
  • G. Dowek, Th. Hardin, C. Kirchner : “Theorem Proving modulo”, Journal of Automated Reasoning, vol. 31 (1), pp. 33-72, (Springer Verlag) (2003)
• 2002
  • G. Dowek, Th. Hardin, C. Kirchner : “Binding Logic: proofs and models”, 9^th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning - LPAR'2002, vol. 2514, Lecture notes in Artificial Intelligence, Tbilisi, Georgia, pp. 130-144, (Springer) (2002)
  • D. Doligez, Th. Hardin, V. Prevosto : “Algebraic Structures and Dependent Records”, TPHOLs'02 - 15^th International Conference on Theorem Proving in Higher-Order logics, vol. 2410, Lecture Notes in Computer Science, Hampton, VA, United States, pp. 298-313, (Springer) (2002)
  • D. Doligez, Th. Hardin, V. Prevosto : “FOC, a certified computer algebra library”, Automath'2002, Edinburgh, United Kingdom (2002)
  • Th. Hardin : “Produire un logiciel de confiance: quelles hypothèses, quelles limites?”, Journées Francophones des Langages Applicatifs, Anglet, France (2002)
• 2001
  • Th. Hardin : “An overview of the FoC project”, MKM 2001 - First International Workshop on Mathematical Knowledge Management, Linz, Austria (2001)
  • S. Boulmé, Th. Hardin, R. Rioboo : “Some Hints for polynomials in the Foc project”, Calculemus 2001, Siena, Italy, pp. 142-154 (2001)
  • G. Dowek, Th. Hardin, C. Kirchner : “HOL-lambda-sigma: an intentional first-order expression of higher-order logic”, Mathematical Structures in Computer Science, vol. 11, pp. 21-45, (Cambridge University Press (CUP)) (2001)
  • G. Dowek, Th. Hardin, C. Kirchner : “A Completeness theorem for an extension of first-order logic with binders”, Workshop Merlin, Mathematics and Computer Science, Leicester, United Kingdom, pp. 49-63 (2001)
• 2000
  • S. Boulmé, Th. Hardin, R. Rioboo : “Polymorphic Data Types, Objects, Modules and Functors: is it too.much.?”, (2000)
  • G. Dowek, Th. Hardin, C. Kirchner : “Higher-order unification via explicit substitutions”, Information and Computation, vol. 157 (1-2), pp. 183-235, (Elsevier) (2000)
  • Ph. Ayrault, M. Guesdon, Th. Hardin : “Méthodologie de développement d’un outil d’évaluation de la sureté du logiciel, en langage OCaml”, Journées Francophones des Langages Applicatifs, INRIA, Mont Saint-Michel, France, pp. 159-171 (2000)
• 1999
  • G. Dowek, Th. Hardin, C. Kirchner : “HOL-λσ: An Intentional First-Order Expression of Higher-Order Logic”, 10^th International Conference, RTA'99, vol. 1631, Lecture Notes in Computer Science, Trento, Italy, pp. 317-331, (Springer) (1999)
  • S. Boulmé, Th. Hardin, D. Hirschkoff, V. Ménissier‑Morain, R. Rioboo : “On the way to certify computer algebra systems”, Calculemus workshop of FLOC'99, vol. 23 (3), Electronic Notes in Theoretical Computer Science, Trento, Italy, pp. 370-385, (Elsevier) (1999)
  • S. Boulmé, Th. Hardin, R. Rioboo : “Modules, Objets et Calcul Formel”, (1999)
  • S. Boulmé, Th. Hardin, R. Rioboo : “Modules Objets et Calcul Formel”, JFLA'99 - Journées francophone des langages applicatifs, Morzine-Avoriaz, France, (Inria) (1999)
• 1998
  • Th. Hardin, B. Mammass : “Proving the Bounded Retransmission Protocol in the Pi-calculus”, INFINITY'98 - 3^rd International Workshop on Verification of Infinite State Systems, Aalborg, Denmark, pp. 68-80 (1998)
  • Th. Hardin, B. Mammass : “Yet Yet on the bounded retransmission protocol”, (1998)
  • Th. Hardin, L. Maranget, B. Pagano : “Functional runtime systems within the lambda-sigma calculus”, Journal of Functional Programming, vol. 8 (2), pp. 131-176, (Cambridge University Press (CUP)) (1998)
  • G. Dowek, Th. Hardin, C. Kirchner : “Holls: an Intentional First-Order Expression of Higher-Order Logic”, 26 pages (1998)
  • G. Dowek, Th. Hardin, C. Kirchner : “Theorem Proving Modulo”, 27 pages (1998)