### PhD thesis

**A framework for defining computational higher-order logics** `new`

École Polytechnique, 2015, Paris

[ pdf | hal | slides ]

Supervisors: G. Dowek and G. Burel

### Publications

**Mixing HOL and Coq in Dedukti**

A. Assaf and R. Cauderlier

Fourth Workshop on Proof Exchange for Theorem Proving, PxTP 2015

[ pdf | slides ]
**Translating HOL Light to Dedukti**

A. Assaf and G. Burel

Fourth Workshop on Proof Exchange for Theorem Proving, PxTP 2015

[ pdf | slides ]
**Conservativity of embeddings in the λΠ-calculus modulo rewriting**

A. Assaf

13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015

[ pdf | slides ]
**A calculus of constructions with explicit subtyping**

A. Assaf

20th International Conference on Types for Proofs and Programs, TYPES 2014

[ pdf | drops ]
**Call-by-value, call-by-name and the vectorial behaviour of the algebraic λ-calculus**

A. Assaf, A. Diaz-Caro, S. Perdrix, C. Tasson, and B. Valiron

In Logical Methods in Computer Science, volume 10, issue 4, 2014

[ pdf | arXiv ]
**Completeness of algebraic CPS simulations**

A. Assaf and S. Perdrix

I7th International Workshop on Developments of Computational Methods, DCM 2011

[ pdf | arXiv ]

### Master’s thesis

**Traduction de HOL en Dedukti**

École Polytechnique, 2012, Paris

[ pdf ]

Advisors: G. Burel and G. Dowek

### Talks

**The chicken and the pencil**

Deducteam seminar, March 26, 2015, Paris

[ slides ]
**Tarski and Coq**

PPS type theory work group, January 7, 2015, Paris

[ slides ]
**Embedding logics in the λΠ-calculus modulo rewriting**

Stockholm logic seminar, October 21, 2014, Stockholm

[ slides ]
**Soundness of embeddings in the λΠ-calculus modulo rewriting**

Parsifal seminar, October 16, 2014, Palaiseau

[ slides ]
**Embedding logics in Dedukti**

KWARC-Deducteam workshop, May 26, 2014, Bremen

[ slides ]
**Coq à la Tarski**

Types 2014, May 12-15, 2014, Paris

[ abstract | slides ]
**Objects and subtyping in the λΠ-calculus modulo**

joint work with R. Cauderlier and C. Dubois, Types 2014, May 12-15, 2014, Paris

[ abstract | slides ]
**A universal proof framework**

Inria Junior Seminar, September 17, 2013, Rocquencourt

[ slides ]
**Translating HOL to Dedukti**

Journées communes LTP - LAC - LAMHA, October 25-26, 2012, Orléans