http://www.aliassaf.info/research/

1<!DOCTYPE html>
2<html>
3<head>
4  <meta charset="utf-8">
5  <meta name="viewport" content="width=device-width, initial-scale=1.0, user-scalable=yes">
6  <title>Research | Ali Assaf</title>
7  <style type="text/css">code{white-space: pre;}</style>
8  <!--[if lt IE 9]>
9    

9<script src="http://html5shim.googlecode.com/svn/trunk/html5.js"></script>

9
10  <![endif]-->
11  <link rel="stylesheet" href="https://maxcdn.bootstrapcdn.com/bootswatch/3.2.0/spacelab/bootstrap.min.css">
12  <link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/8.1/styles/paraiso.light.min.css">
13  <link rel="stylesheet" href="/assets/main.css">
14</head>
15<body>
16<div class="container">
17<div class="header"></div>
18<ul class="nav nav-tabs">
19<li role="presentation"><a href="/">Home</a></li>
20<li role="presentation"><a href="/research/">Research</a></li>
21<li role="presentation"><a href="/teaching/">Teaching</a></li>
22<li role="presentation"><a href="/software/">Software</a></li>
23</ul>
24<h1 id="research">Research</h1>
25
26<h3 id="phd-thesis">PhD thesis</h3>
27
28<ul>
29  <li><strong>A framework for defining computational higher-order logics</strong> <code>new</code> <br />
30École Polytechnique, 2015, Paris <br />
31[ <a href="/research/thesis.pdf">pdf</a> | <a href="https://hal.inria.fr/tel-01235303">hal</a> | <a href="/research/thesis-slides.pdf">slides</a> ] <br />
32Supervisors: <a href="https://who.rocq.inria.fr/Gilles.Dowek/">G. Dowek</a> and <a href="http://www.ensiie.fr/~guillaume.burel/">G. Burel</a></li>
33</ul>
34
35<h3 id="publications">Publications</h3>
36
37<ul>
38  <li><strong>Mixing HOL and Coq in Dedukti</strong> <br />
39A. Assaf and R. Cauderlier <br />
40Fourth Workshop on Proof Exchange for Theorem Proving, PxTP 2015 <br />
41[ <a href="/research/dedukti-interop-pxtp-2015.pdf">pdf</a> | <a href="/research/dedukti-interop-pxtp-2015-slides.pdf">slides</a> ]</li>
42  <li><strong>Translating HOL Light to Dedukti</strong> <br />
43A. Assaf and G. Burel <br />
44Fourth Workshop on Proof Exchange for Theorem Proving, PxTP 2015 <br />
45[ <a href="/research/translating-hollight-dedukti-pxtp-2015.pdf">pdf</a> | <a href="/research/holide-pxtp-2015-slides.pdf">slides</a> ]</li>
46  <li><strong>Conservativity of embeddings in the λΠ-calculus modulo rewriting</strong> <br />
47A. Assaf <br />
4813th International Conference on Typed Lambda Calculi and Applications, TLCA 2015 <br />
49[ <a href="/research/conservativity-embeddings-tlca-2015.pdf">pdf</a> | <a href="/research/conservativity-embeddings-tlca-2015-slides.pdf">slides</a> ]</li>
50  <li><strong>A calculus of constructions with explicit subtyping</strong> <br />
51A. Assaf <br />
5220th International Conference on Types for Proofs and Programs, TYPES 2014 <br />
53[ <a href="/research/coc-explicit-subtyping-types-2014.pdf">pdf</a> | <a href="http://drops.dagstuhl.de/portals/extern/index.php?semnr=15017">drops</a> ]</li>
54  <li><strong>Call-by-value, call-by-name and the vectorial behaviour of the algebraic λ-calculus</strong> <br />
55A. Assaf, <a href="https://who.rocq.inria.fr/Alejandro.Diaz-Caro/">A. Diaz-Caro</a>, <a href="http://membres-lig.imag.fr/perdrix/">S. Perdrix</a>, <a href="http://www.pps.univ-paris-diderot.fr/~tasson/">C. Tasson</a>, and <a href="http://www.monoidal.net/">B. Valiron</a> <br />
56In Logical Methods in Computer Science, volume 10, issue 4, 2014 <br />
57[ <a href="/research/cbv-cbn-algebraic-lmcs-2014.pdf">pdf</a> | <a href="http://arxiv.org/abs/1005.2897">arXiv</a> ]</li>
58  <li><strong>Completeness of algebraic CPS simulations</strong> <br />
59A. Assaf and <a href="http://membres-lig.imag.fr/perdrix/">S. Perdrix</a> <br />
60I7th International Workshop on Developments of Computational Methods, DCM 2011 <br />
61[ <a href="/research/completeness-algebraic-cps-dcm-2011.pdf">pdf</a> | <a href="http://arxiv.org/abs/1207.7146">arXiv</a> ]</li>
62</ul>
63
64<h3 id="masters-thesis">Master’s thesis</h3>
65
66<ul>
67  <li>
68    <p><strong>Traduction de HOL en Dedukti</strong> <br />
69École Polytechnique, 2012, Paris <br />
70[ <a href="/research/rapport-master-2012.pdf">pdf</a> ]</p>
71
72    <p>Advisors: <a href="http://www.ensiie.fr/~guillaume.burel/">G. Burel</a> and <a href="https://who.rocq.inria.fr/Gilles.Dowek/">G. Dowek</a></p>
73  </li>
74</ul>
75
76<h3 id="talks">Talks</h3>
77
78<ul>
79  <li><strong>The chicken and the pencil</strong> <br />
80Deducteam seminar, March 26, 2015, Paris <br />
81[ <a href="/research/krajono-deducteam-2015-slides.pdf">slides</a> ]</li>
82  <li><strong>Tarski and Coq</strong> <br />
83PPS type theory work group, January 7, 2015, Paris <br />
84[ <a href="/research/tarski-and-coq-pps-2015-slides.pdf">slides</a> ]</li>
85  <li><strong>Embedding logics in the λΠ-calculus modulo rewriting</strong> <br />
86Stockholm logic seminar, October 21, 2014, Stockholm <br />
87[ <a href="/research/embedding-logics-stockholm-2014.pdf">slides</a> ]</li>
88  <li><strong>Soundness of embeddings in the λΠ-calculus modulo rewriting</strong> <br />
89Parsifal seminar, October 16, 2014, Palaiseau <br />
90[ <a href="/research/conservativity-embeddings-parsifal-2014-slides.pdf">slides</a> ]</li>
91  <li><strong>Embedding logics in Dedukti</strong> <br />
92KWARC-Deducteam workshop, May 26, 2014, Bremen <br />
93[ <a href="/research/embedding-logics-kwarc-2014-slides.pdf">slides</a> ]</li>
94  <li><strong>Coq à la Tarski</strong> <br />
95Types 2014, May 12-15, 2014, Paris <br />
96[ <a href="/research/coq-tarski-types-2014-abstract.pdf">abstract</a> |
97  <a href="/research/coq-tarski-types-2014-slides.pdf">slides</a> ]</li>
98  <li><strong>Objects and subtyping in the λΠ-calculus modulo</strong> <br />
99joint work with <a href="https://who.rocq.inria.fr/Raphael.Cauderlier/">R. Cauderlier</a> and <a href="http://www.ensiie.fr/~dubois/">C. Dubois</a>,
100Types 2014, May 12-15, 2014, Paris <br />
101[ <a href="/research/object-subtyping-types-2014-abstract.pdf">abstract</a> |
102  <a href="/research/object-subtyping-types-2014-slides.pdf">slides</a> ]</li>
103  <li><strong>A universal proof framework</strong> <br />
104<a href="http://pauillac.inria.fr/~protzenk/semdoc/">Inria Junior Seminar</a>, September 17, 2013, Rocquencourt <br />
105[ <a href="/research/universal-proof-framework-semdoc-2013-slides.pdf">slides</a> ]</li>
106  <li><strong>Translating HOL to Dedukti</strong> <br />
107Journées communes LTP - LAC - LAMHA, October 25-26, 2012, Orléans</li>
108</ul>
109
110
111<div class="footer"><p>
112<hr />
113Built using
114  <a href="https://getbootstrap.com/">bootstrap</a>,
115  <a href="http://highlightjs.org/">highlightjs</a>,
116  <a href="http://mathjax.org/">mathjax</a>, and
117  <a href="http://jekyllrb.com/">jekyll</a>
118| Copyright © 2014 Ali Assaf
119</p>
120</div>
121</div>
122<!-- Placed at the end of the document so the pages load faster -->

123<script type="text/javascript" src="https://maxcdn.bootstrapcdn.com/bootstrap/3.2.0/js/bootstrap.min.js"></script>

123

124<script type="text/javascript" src="https://cdn.mathjax.org/mathjax/latest/MathJax.js?config=TeX-AMS-MML_HTMLorMML"></script>

124

125<script type="text/javascript" src="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/8.1/highlight.min.js"></script>

125

126<script>hljs.initHighlightingOnLoad();</script>

126
127</body>
128</html>