An ML-Like Module System for the Synchronous Language SIGNAL. - David Nowak; Jean-Pierre Talpin; Thierry Gautier; Paul Le Guernic (Euro-Par, 1997)

A Synchronous Semantics of Higher-Order Processes for Modeling Reconfigurable Reactive Systems. - Jean-Pierre Talpin; David Nowak (FSTTCS, 1998)

Co-inductive Axiomatization of a Synchronous Language. - David Nowak; Jean-René Beauvais; Jean-Pierre Talpin (TPHOLs, 1998)

Synchronous Structures. - David Nowak; Jean-Pierre Talpin; Paul Le Guernic (CONCUR, 1999)

A Unifying Approach to Data-Independence. - Ranko Lazic 001; David Nowak (CONCUR, 2000)

Specification and Verification of a Steam-Boiler with Signal-Coq. - Mickaël Kerboeuf; David Nowak; Jean-Pierre Talpin (TPHOLs, 2000)

Our perspective on the Alliance Program's benefits. - Dona Crawford; Donald McCoy; David Nowak (Comput. Sci. Eng., 2000)

Logical Relations for Dynamic Name Creation. - Yu Zhang; David Nowak (CSL, 2003)

Formal Proof of a Polychronous Protocol for Loosely Time-Triggered Architectures. - Mickaël Kerboeuf; David Nowak; Jean-Pierre Talpin (ICFEM, 2003)

On a Semantic Definition of Data Independence . - Ranko Lazic 001; David Nowak (TLCA, 2003)

Complete Lax Logical Relations for Cryptographic Lambda-Calculi. - Jean Goubault-Larrecq; Slawomir Lasota 001; David Nowak; Yu Zhang (CSL, 2004)

On Completeness of Logical Relations for Monadic Types. - Slawomir Lasota 001; David Nowak; Yu Zhang (ASIAN, 2006)

Synchronous structures. - David Nowak (Inf. Comput., 2006)

A Framework for Game-Based Security Proofs. - David Nowak (IACR Cryptol. ePrint Arch., 2007)

On the freeze quantifier in Constraint LTL: Decidability and complexity. - Stéphane Demri; Ranko Lazic 001; David Nowak (Inf. Comput., 2007)

Reasoning about Transfinite Sequences. - Stéphane Demri; David Nowak (Int. J. Found. Comput. Sci., 2007)

On Formal Verification of Arithmetic-Based Cryptographic Primitives. - David Nowak (ICISC, 2008)

Logical relations for monadic types. - Jean Goubault-Larrecq; Slawomir Lasota 001; David Nowak (Math. Struct. Comput. Sci., 2008)

Certifying Assembly with Formal Cryptographic Proofs: the Case of BBS. - Reynald Affeldt; David Nowak; Kiyoshi Yamada (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2009)

A calculus for game-based security proofs. - David Nowak; Yu Zhang (IACR Cryptol. ePrint Arch., 2010)

A Formalization of Polytime Functions. - Sylvain Heraud; David Nowak (ITP, 2011)

Component-based development and sensitivity analyses of an air pollutant dry deposition model. - Satoshi Hirabayashi; Charles Kroll; David Nowak (Environ. Model. Softw., 2011)

Formal network packet processing with minimal fuss: invertible syntax descriptions at work. - Reynald Affeldt; David Nowak; Yutaka Oiwa (PLPV, 2012)

Certifying assembly with formal security proofs: The case of BBS. - Reynald Affeldt; David Nowak; Kiyoshi Yamada (Sci. Comput. Program., 2012)

Implicit Computational Complexity and Applications: Resource Control, Security, Real-Number Computation (NII Shonan Meeting 2013-13). - Akitoshi Kawamura; Jean-Yves Marion; David Nowak (NII Shonan Meet. Rep., 2013)

Summer School on Coq (NII Shonan Meeting 2014-9). - Pierre Castéran; Jacques Garrigue; David Nowak (NII Shonan Meet. Rep., 2014)

Verifying Reachability-Logic Properties on Rewriting-Logic Specifications. - Dorel Lucanu; Vlad Rusu; Andrei Arusoaie; David Nowak (Logic, Rewriting, and Concurrency, 2015)

Formal security proofs with minimal fuss: Implicit computational complexity at work. - David Nowak; Yu Zhang (Inf. Comput., 2015)

A Certified Procedure for RL Verification. - Andrei Arusoaie; David Nowak; Vlad Rusu; Dorel Lucanu (SYNASC, 2017)

Formal proof of polynomial-time complexity with quasi-interpretations. - Hugo Férée; Samuel Hym; Micaela Mayero; Jean-Yves Moyen; David Nowak (CPP, 2018)

Formalising Executable Specifications of Low-Level Systems. - Paolo Torrini; David Nowak; Narjes Jomaa; Mohamed Sami Cherif (VSTTE, 2018)

Proof-Oriented Design of a Separation Kernel with Minimal Trusted Computing Base. - Narjes Jomaa; Paolo Torrini; David Nowak; Gilles Grimaud; Samuel Hym (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2018)

Formal proof of dynamic memory isolation based on MMU. - Narjes Jomaa; David Nowak; Gilles Grimaud; Samuel Hym (Sci. Comput. Program., 2018)

A Hierarchy of Monadic Effects for Program Verification Using Equational Reasoning. - Reynald Affeldt; David Nowak; Takafumi Saikawa (MPC, 2019)

Extending Equational Monadic Reasoning with Monad Transformers. - Reynald Affeldt; David Nowak (TYPES, 2020)

A trustful monad for axiomatic reasoning with probability and nondeterminism. - Reynald Affeldt; Jacques Garrigue; David Nowak; Takafumi Saikawa (J. Funct. Program., 2021)

(Co)inductive proof systems for compositional proofs in reachability logic. - Vlad Rusu; David Nowak (J. Log. Algebraic Methods Program., 2021)

Defining Corecursive Functions in Coq Using Approximations. - Vlad Rusu; David Nowak (ECOOP, 2022)

A Formal Correctness Proof for an EDF Scheduler Implementation. - Florian Vanhems; Vlad Rusu; David Nowak; Gilles Grimaud (RTAS, 2022)

Defining Corecursive Functions in Coq Using Approximations (Artifact). - Vlad Rusu; David Nowak (Dagstuhl Artifacts Ser., 2022)

While Loops in Coq. - David Nowak; Vlad Rusu (FROM, 2023)

Trust in Times of Cyber Crisis: Understanding Organizational Trust Repair in the Public Sector. - David Nowak; Bettina Distel (EGOV, 2024)

Capturing trust in public service encounters: Mapping trust along life event citizen journeys. - David Nowak (RVI, 2024)

Formal definitions and proofs for partial (co)recursive functions. - Horatiu Cheval; David Nowak; Vlad Rusu (J. Log. Algebraic Methods Program., 2024)