@phdthesis{C-phd2016,
author = {Cauderlier, Rapha{\"e}l},
title = {{Object-Oriented Mechanisms for Interoperability between Proof Systems}},
school = {{Conservatoire National Des Arts et M{\'e}tiers, Paris}},
type = {Th{\`e}se de doctorat},
year = 2016,
month = oct,
url = {https://hal.inria.fr/tel-01415945/},
pdf = {https://hal.inria.fr/tel-01415945/file/main.pdf}
}
@inproceedings{Halmagrand-ictac16,
address = {Taipei, Taiwan},
month = oct,
volume = 9965,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Alves Sampaio, Cesar and Wang, Farn},
acronym = {{ICTAC}'16},
booktitle = {{P}roceedings of the 13th {I}nternational {C}olloquium on
{T}heoretical {A}spects of {C}omputing ({ICTAC}'16)},
author = {Halmagrand, Pierre},
title = {{{Soundly Proving B Method Formulae Using Typed Sequent Calculus}}},
pages = {196-213},
year = {2016},
doi = {10.1007/978-3-319-46750-4_12},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/Halmagrand-ictac2016.pdf},
url = {https://hal.archives-ouvertes.fr/hal-01342849},
abstract = {The B Method is a formal method mainly used in the railway industry to specify and develop safety-critical software.
To guarantee the consistency of a B project, one decisive challenge is to show correct a large amount of proof obligations, which are mathematical formulae
expressed in a classical set theory extended with a specific type system. To improve automated theorem proving in the B Method, we propose to use a
first-order sequent calculus extended with a polymorphic type system, which is in particular the output proof-format of the tableau-based automated
theorem prover Zenon. After stating some modifications of the B syntax and defining a sound elimination of comprehension sets, we propose a
translation of B formulae into a polymorphic first-order logic format. Then, we introduce the typed sequent calculus used by Zenon, and show
that Zenon proofs can be translated to proofs of the initial B formulae in the B proof system.}
}
@comment{{B-arxiv16,
author = Bollig, Benedikt,
affiliation = aff-LSVmexico,
title = One-Counter Automata with Counter Visibility,
institution = Computing Research Repository,
number = 1602.05940,
month = feb,
nmonth = 2,
year = 2016,
type = RR,
axeLSV = mexico,
NOcontrat = "",
url = http://arxiv.org/abs/1602.05940,
PDF = "http://www.lsv.fr/Publis/PAPERS/PDF/B-arxiv16.pdf",
lsvdate-new = 20160222,
lsvdate-upd = 20160222,
lsvdate-pub = 20160222,
lsv-category = "rapl",
wwwpublic = "public and ccsb",
note = 18~pages,
abstract = "In a one-counter automaton (OCA), one can read a letter
from some finite alphabet, increment and decrement the counter by
one, or test it for zero. It is well-known that universality and
language inclusion for OCAs are undecidable. We consider here OCAs
with counter visibility: Whenever the automaton produces a letter,
it outputs the current counter value along with~it. Hence, its
language is now a set of words over an infinite alphabet. We show
that universality and inclusion for that model are in PSPACE, thus
no harder than the corresponding problems for finite automata, which
can actually be considered as a special case. In fact, we show that
OCAs with counter visibility are effectively determinizable and
closed under all boolean operations. As~a~strict generalization, we
subsequently extend our model by registers. The general nonemptiness
problem being undecidable, we impose a bound on the number of
register comparisons and show that the corresponding nonemptiness
problem is NP-complete.",
}}
@techreport{DD-arxiv16,
author = {D{\'i}az{-}Caro, Alejandro and Dowek, Gilles},
title = {Quantum superpositions and projective measurement in
the lambda calculus},
institution = {Computing Research Repository},
number = {1601.04294},
year = {2016},
month = jan,
type = {Research Report},
url = {http://arxiv.org/abs/1601.04294},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DD-arxiv16.pdf},
note = {22~pages},
abstract = {We propose an extension of simply typed lambda-calculus to
handle some properties of quantum computing. The equiprobable quantum
superposition is taken as a commutative pair and the quantum measurement
as a non-deterministic projection over it. Destructive interferences are
achieved by introducing an inverse symbol with respect to pairs. The
no-cloning property is ensured by using a combination of syntactic
linearity with linear logic. Indeed, the syntactic linearity is enough for
unitary gates, while a function measuring its argument needs to enforce
that the argument is used only once.}
}
@inproceedings{G-fossacs17,
address = {Uppsala, Sweden},
month = apr,
year = 2017,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Esparza, Javier and Murawski, Andrzej},
acronym = {{FoSSaCS}'17},
booktitle = {{P}roceedings of the 20th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'17)},
author = {Gilbert, Fr{\'e}d{\'e}ric},
title = {Automated Constructivization of Proofs},
pages = {480-495},
url = {https://hal.inria.fr/hal-01516788},
pdf = {https://hal.inria.fr/hal-01516788/file/constructivization.pdf},
doi = {10.1007/978-3-662-54458-7_28},
abstract = {No computable function can output a constructive proof from a classical one whenever its associated theorem also holds constructively. We show in this paper that it is however possible, in practice, to turn a large amount of classical proofs into constructive ones. We describe for this purpose a linear-time constructivization algorithm which is provably complete on large fragments of predicate logic.}
}
@inproceedings{G-itp17,
address = {Bras{\'{\i}}lia, Brazil},
year = 2017,
month = sep,
volume = 10499,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Ayala{-}Rinc{\'{o}}n, Mauricio and Mu{\~{n}}oz, C{\'{e}}sar A.},
acronym = {{ITP}'17},
booktitle = {{P}roceedings of the 8th {I}nternational {C}onference on
{I}nteractive {T}heorem {P}roving ({ITP}'17)},
author = {Gilbert, Fr{\'e}d{\'e}ric},
title = {Proof Certificates in {PVS}},
pages = {262-268},
url = {https://hal.inria.fr/hal-01673517},
pdf = {https://hal.inria.fr/hal-01673517/file/main.pdf},
doi = {10.1007/978-3-319-66107-0_17},
abstract = {The purpose of this work is to allow the proof system PVS to export proof certificates that can be checked externally. This is done through the instrumentation of PVS to record detailed proofs step by step during the proof search process. At the current stage of this work, proofs can be built for any PVS theory. However, some reasoning steps rely on unverified assumptions. For a restricted fragment of PVS, the proofs are exported to the universal proof checker Dedukti, and the unverified assumptions are proved externally using the automated theorem prover MetiTarski.}
}
@inproceedings{B-ocaml17,
author = {Bury, Guillaume},
title = {{mSAT: An OCaml SAT Solver}},
booktitle = {{OCaml Users and Developers Workshop}},
nopages = {},
noeditor = {},
month = sep,
year = 2017,
address = {Oxford, UK},
url = {https://hal.inria.fr/hal-01670765},
pdf = {https://hal.inria.fr/hal-01670765/file/poster.pdf},
abstract = {mSAT: a SAT solving library in OCaml. It solves the satisfibility of propositional clauses. It is Modular: the user provides the theory. And it produces formal proofs.},
note = {Poster}
}
@inproceedings{JS-lpar17,
address = {Maun, Botswana},
month = may,
volume = {46},
series = {EPiC Series in Computing},
publisher = {EasyChair},
editor = {Eiter, Thomas and Sands, David},
acronym = {{LPAR}'17},
booktitle = {{P}roceedings of the 21st {I}nternational
{C}onference on {L}ogic for {P}rogramming,
{A}rtificial {I}ntelligence, and {R}easoning
({LPAR}'17)},
author = {Jouannaud, Jean-Pierre and Strub, Pierre-Yves},
title = {{Coq without Type Casts: A Complete Proof of Coq Modulo Theory}},
pages = {474-489},
year = {2017},
pdf = {https://hal.inria.fr/hal-01664457/file/final-version.pdf},
url = {https://easychair.org/publications/paper/BKQ},
abstract = {Incorporating extensional equality into a dependent intensional type system such as the Calculus of Constructions provides with stronger type-checking capabilities and makes the proof development closer to intuition. Since strong forms of extensionality lead to undecidable type-checking, a good trade-off is to extend intensional equality with a decidable first-order theory T, as done in CoqMT, which uses matching modulo T for the weak and strong elimination rules, we call these rules T-elimination. So far, type-checking in CoqMT is known to be decidable in presence of a cumulative hierarchy of universes and weak T-elimination. Further, it has been shown by Wang with a formal proof in Coq that consistency is preserved in presence of weak and strong elimination rules, which actually implies consistency in presence of weak and strong T-elimination rules since T is already present in the conversion rule of the calculus.
\par
We justify here CoqMT's type-checking algorithm by showing strong normalization as well as the Church-Rosser property of \(\beta\)-reductions augmented with CoqMT's weak and strong T-elimination rules. This therefore concludes successfully the meta-theoretical study of CoqMT.}
}
@inproceedings{Dowek-icalp17,
address = {Warsaw, Poland},
month = jul,
volume = {80},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Chatzigiannakis, Ioannis and Indyk, Piotr and Muscholl, Anca and Kuhn, Fabian},
acronym = {{ICALP}'17},
booktitle = {{P}roceedings of the 44th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'17)},
author = {Dowek, Gilles},
title = {Models and termination of proof reduction in the \(\lambda\Pi\)-calculus modulo theory},
pages = {109:1-109:14},
year = {2017},
doi = {10.4230/LIPIcs.ICALP.2017.109},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2017/7391/pdf/LIPIcs-ICALP-2017-109.pdf},
url = {http://drops.dagstuhl.de/opus/volltexte/2017/7391},
abstract = {We define a notion of model for the \(\lambda\Pi\)-calculus modulo theory and prove a soundness theorem. We then use this notion to define a notion of super-consistent theory and prove that proof reduction terminates in the \(\lambda\Pi\)-calculus modulo any super-consistent theory. We prove this way the termination of proof reduction in several theories including Simple type theory and the Calculus of constructions.}
}
@inproceedings{AMP-lfmtp16,
address = {Porto, Portugal},
month = jun,
publisher = {ACM Press},
editor = {Dowek, Gilles and Licata, Daniel R. and Alves, Sandra},
acronym = {{LFMTP}'16},
booktitle = {Proceedings of the 11th {I}nternational {W}orkshop on {L}ogical {F}rameworks and
{M}eta-{L}anguages: {T}heory and {P}ractice ({LFMTP}'16)},
author = {Cauderlier, Rapha{\"e}l},
title = {{{A Rewrite System for Proof Constructivization}}},
pages = {2:1-2:7},
year = {2016},
doi = {10.1007/978-3-319-40578-0\_5},
url = {https://hal.inria.fr/hal-01420634/},
pdf = {https://hal.inria.fr/hal-01420634/file/LFMTP_2016.pdf},
abstract = {Proof constructivization is the problem of automatically extracting constructive proofs out of classical proofs. This process is required when classical theorem provers are integrated in intuitionistic proof assistants. We use the ability of rewrite systems to represent partial functions to implement heuristics for proof constructivization in Dedukti, a logical framework based on rewriting in which proofs are first-class objects which can be the subject of computation. We benchmark these heuristics on the proofs output by the automated theorem prover Zenon on the TPTP library of problems.}
}
@inproceedings{AMP-rc16,
address = {Bologna, Italy},
month = jul,
volume = 9720,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Lanese, Ivan and Devitt, Simon},
acronym = {{RC}'16},
booktitle = {8th Conference on Reversible Computation (RC'16)},
author = {Arrighi, Pablo and Martiel, Simon and Perdrix, Simon},
title = {{{Reversible Causal Graph Dynamics}}},
pages = {73-88},
year = {2016},
doi = {10.1007/978-3-319-40578-0\_5},
url = {https://hal.archives-ouvertes.fr/hal-01361427},
abstract = {Causal Graph Dynamics extend Cellular Automata to arbitrary , bounded-degree, time-varying graphs. The whole graph evolves in discrete time steps, and this global evolution is required to have a number of physics-like symmetries: shift-invariance (it acts everywhere the same) and causality (information has a bounded speed of propagation). We add a further physics-like symmetry, namely reversibility.}
}
@inproceedings{ADJL-hatt2016,
author = {Assaf, Ali and Dowek, Gilles and Jouannaud, Jean-Pierre and Liu, Jiaxiang},
title = {{{Encoding Proofs in Dedukti: the case of Coq proofs}}},
nopages = {},
booktitle = {Preliminary Proceedings of the 1st International Workshop on Hammers for Type Theories (HaTT'16)},
year = {2016},
address = {Coimbra, Portugal},
url = {https://hal.inria.fr/hal-01330980},
pdf = {https://hal.inria.fr/hal-01330980/file/HaTT_2016_paper_3.pdf},
abstract = {A main ambition of the Inria project Dedukti is to serve as a common language for representing and type checking proof objects originating from other proof systems. Encoding these proof objects makes heavy use of the rewriting capabilities of LambdaPiModulo, the formal system on which Dedukti is based. So far, the proofs generated by two automatic proof systems, Zenon and iProver, have been encoded, and can therefore be read and checked by Dedukti. But Dedukti goes far beyond this so-called hammering technique of sending goals to automated provers. Proofs from HOL and Matita can be encoded as well. Some Coq?s proofs can be encoded already, when they do not use universe polymorphism. Our ambition here is to close this remaining gap. To this end, we describe a rewrite-based encoding in LambdaPiModulo of the Calculus of Constructions with a cumulative hierarchy of predicative universes above Prop, which is confluent on open terms.}
}
@inproceedings{ADJL-hor2016,
author = {Assaf, Ali and Dowek, Gilles and Jouannaud, Jean-Pierre and Liu, Jiaxiang},
title = {{{Untyped Confluence in Dependent Type Theories}}},
nopages = {},
booktitle = {Proceedings of the 8th International Workshop on Higher-Order Rewriting (HOR'16)},
year = {2016},
address = {Porto, Portugal},
url = {https://hal.inria.fr/hal-01330955},
pdf = {https://hal.inria.fr/hal-01330955/file/HOR_2016_paper.pdf},
abstract = {We investigate techniques based on van Oostrom's decreasing diagrams that reduce confluence proofs to the checking of critical pairs in the absence of termination properties, which are useful in dependent type calculi to prove confluence on untyped terms. These techniques are applied to a complex example originating from practice: a faithful encoding, in an extension of LF with rewrite rules on objects and types, of a subset of the calculus of inductive constructions with a cumulative hierarchy of predicative universes above Prop. The rules may be first-order or higher-order, plain or modulo, non-linear on the right or on the left. Variables which occur non-linearly in lefthand sides of rules must take their values in confined types: in our example, the natural numbers. The first-order rules are assumed to be terminating and confluent modulo some theory: in our example, associativity, commutativity and identity. Critical pairs involving higher-order rules must satisfy van Oostrom's decreasing diagram condition wrt their indexes taken as labels.}
}
@inproceedings{A-types2016,
address = {Novi Sad, Serbia},
volume = {97},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Ghilezan, Silvia and Ivetic, Jelena},
acronym = {{TYPES}'16},
booktitle = {{P}roceedings of the 22nd {I}nternational {C}onference on {T}ypes for {P}roofs and {P}rograms
({TYPES}'16)},
author = {Assaf, Ali and Burel, Guillaume and Cauderlier, Rapha{\"e}l and Delahaye, David and Dowek, Gilles and Dubois, Catherine and Gilbert, Fr{\'e}d{\'e}ric and Halmagrand, Pierre and Hermant, Olivier and Saillard, Ronan},
title = {{{Expressing theories in the {{\(\lambda\Pi\)}}-calculus modulo theory and in the Dedukti system}}},
year = {2016},
note = {To appear}
}
@unpublished{D-preprint2016,
title = {{Rules and derivations in an elementary logic course}},
author = {Dowek, Gilles},
note = {preprint},
year = {2016},
month = jan,
url = {https://hal.inria.fr/hal-01252124/},
pdf = {https://hal.inria.fr/hal-01252124/file/ttl.pdf},
abstract = {When teaching an elementary logic course to students who have a general scientific background but have never been exposed to logic, we have to face the problem that the notions of deduction rule and of derivation are completely new to them, and are related to nothing they already know, unlike, for instance, the notion of model, that can be seen as a generalization of the notion of algebraic structure. In this note, we defend the idea that one strategy to introduce these notions is to start with the notion of inductive definition [1]. Then, the notion of derivation comes naturally. We also defend the idea that derivations are pervasive in logic and that defining precisely this notion at an early stage is a good investment to later define other notions in proof theory, computability theory, automata theory, ... Finally, we defend the idea that to define the notion of derivation precisely, we need to distinguish two notions of derivation: labeled with elements and labeled with rule names. This approach has been taken in [2].}
}
@unpublished{AD-preprint2016,
title = {{What is the Planck constant the magnitude of?}},
author = {Arrighi, Pablo and Dowek, Gilles},
note = {preprint},
year = {2016},
month = dec,
url = {https://hal.inria.fr/hal-01421711},
pdf = {https://hal.inria.fr/hal-01421711/file/planck.pdf},
abstract = {The Planck constant is the minimal area of one bit.}
}
@inproceedings{CD-ictac16,
address = {Taipei, Taiwan},
month = oct,
volume = 9965,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Alves Sampaio, Cesar and Wang, Farn},
acronym = {{ICTAC}'16},
booktitle = {{P}roceedings of the 13th {I}nternational {C}olloquium on
{T}heoretical {A}spects of {C}omputing ({ICTAC}'16)},
author = {Cauderlier, Rapha{\"e}l and Dubois, Catherine},
title = {{{ML Pattern-Matching, Recursion, and Rewriting: From FoCaLiZe to Dedukti}}},
pages = {459-468},
year = {2016},
pdf = {https://hal.inria.fr/hal-01420638/file/ICTAC_2016.pdf},
url = {https://hal.inria.fr/hal-01420638/},
abstract = {The programming environment FoCaLiZe allows the user to specify, implement, and prove programs with the help of the theorem prover Zenon. In the actual version, those proofs are verified by Coq. In this paper we propose to extend the FoCaLiZe compiler by a backend to the Dedukti language in order to benefit from Zenon Modulo, an extension of Zenon for Deduction modulo. By doing so, FoCaLiZe can benefit from a technique for finding and verifying proofs more quickly. The paper focuses mainly on the process that overcomes the lack of local pattern-matching and recursive definitions in Dedukti.}
}
@mastersthesis{m2-thire,
author = {Thir{\'e}, Fran{\c{c}}ois},
title = {Reverse engineering on arithmetic proofs},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = {2016},
month = aug,
url = {https://hal.inria.fr/hal-01424816},
pdf = {https://hal.inria.fr/hal-01424816/file/main.pdf},
note = {26~pages}
}
@phdthesis{ph-phd2016,
author = {Halmagrand, Pierre},
title = {{Automated Deduction and Proof Certification for the B Method}},
school = {{Conservatoire National Des Arts et M{\'e}tiers, Paris}},
type = {Th{\`e}se de doctorat},
year = 2016,
month = dec,
url = {https://hal.inria.fr/tel-01420460/}
}
@inproceedings{AD-dcm15,
address = {Cali, Colombia},
month = mar,
volume = 204,
series = {Electronic Proceedings in Theoretical Computer Science},
editor = {Mu\~noz, C\'esar A. and P\'erez, Jorge A.},
acronym = {{DCM}'15},
booktitle = {{P}roceedings of the 11th {I}nternational {W}orkshop on
{D}evelopments in {C}omputational {M}odels ({DCM}'15)},
author = {Arrighi, Pablo and Dowek, Gilles},
doi = {10.4204/EPTCS.204.1},
pages = {1-10},
title = {Free fall and cellular automata},
url = {https://hal.inria.fr/hal-01421712},
year = {2016},
abstract = {Three reasonable hypotheses lead to the thesis that physical phenomena can be described and simulated with cellular automata. In this work, we attempt to describe the motion of a particle upon which a constant force is applied, with a cellular automaton, in Newtonian physics, in Special Relativity, and in General Relativity. The results are very different for these three theories.}
}
@inproceedings{BG-wst18,
address = {Oxford, UK},
month = jul,
editor = {Lucas, Salvador},
acronym = {{WST}'18},
booktitle = {{P}roceedings of the 16th {I}nternational {W}orkshop on {T}ermination
({WST}'18)},
author = {Blanqui, Fr{\'e}d{\'e}ric and Genestier, Guillaume},
title = {Termination of $\lambda \Pi$ modulo rewriting using the size-change principle},
pages = {10--14},
year = 2018,
pdf = {https://hal.inria.fr/hal-01944731/file/main.pdf}
}
@inproceedings{Thire-lfmtp2018,
address = {Oxford, UK},
month = jul,
year = 2018,
publisher = {ACM Press},
editor = {Blanqui, Fr{\'e}d{\'e}ric and Reis, Giselle},
acronym = {{LFMTP}'18},
booktitle = {Proceedings of the 13th {I}nternational {W}orkshop on {L}ogical {F}rameworks and
{M}eta-{L}anguages: {T}heory and {P}ractice ({LFMTP}'18)},
author = {Thir{\'e}, Fran{\c{c}}ois},
title = {{S}haring a {L}ibrary between {P}roof {A}ssistants: {R}eaching out to the {HOL}
{F}amily *},
pages = {57--71},
url = {http://eptcs.web.cse.unsw.edu.au/paper.cgi?LFMTP2018.5},
pdf = {https://hal.inria.fr/hal-01929714/file/sttforall-lfmtp.pdf},
doi = {10.4204/EPTCS.274.4}
}
@inproceedings{Burel-mfcs2018,
address = {Liverpool, UK},
month = aug,
volume = {117},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Potapov, Igor and Spirakis, Paul and Worrell, James},
acronym = {{MFCS}'18},
booktitle = {{P}roceedings of the 42nd
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'18)},
author = {Burel, Guillaume},
title = {Linking Focusing and Resolution with Selection},
pages = {9:1--9:14},
year = {2018},
doi = {10.4230/LIPIcs.MFCS.2018.9},
url = {https://hal.inria.fr/hal-01670476},
pdf = {https://hal.inria.fr/hal-01670476/file/lipics.pdf},
futureannote = {Keywords: logic in computer science, automated deduction,
proof theory, sequent calculus, refinements of resolution, deduction
modulo theory, polarization}
}
@inproceedings{CLS-jfla19,
address = {Lamoura, France},
month = jan,
year = 2019,
editor = {Nicolas Magaud and Zaynah Dargaye},
acronym = {{JFLA}'19},
booktitle = {{A}ctes des 30{\`e}mes {J}ourn{\'e}es
{F}rancophones sur les {L}angages
{A}pplicatifs
({JFLA}'19)},
author = {Simon Colin and Rodolphe Lepigre and Gabriel Scherer},
title = {{Unboxing Mutually Recursive Type Definitions}},
pdf = {https://lepigre.fr/files/publications/CLS2019.pdf},
abstract = {In modern OCaml, single-argument datatype declarations (variants with a single constructor, records with a single immutable field) can sometimes be ''unboxed''. This means that their memory representation is the same as their single argument, omitting an indirection through the variant or record constructor, thus achieving better memory efficiency. However, in the case of generalized/guarded algebraic datatypes (GADTs), unboxing is not always possible due to a subtle assumption about the runtime representation of OCaml values. The current correctness check is incomplete, rejecting many valid definitions, in particular those involving mutually-recursive datatype declarations. In this paper, we explain the notion of separability as a semantic for the unboxing criterion, and propose a set of inference rules to check separability. From these inference rules, we derive a new implementation of the unboxing check that properly supports mutually-recursive definitions.},
note = {To appear}
}
@inproceedings{LR-lfmtp2018,
address = {Oxford, UK},
month = jul,
year = 2018,
publisher = {ACM Press},
editor = {Blanqui, Fr{\'e}d{\'e}ric and Reis, Giselle},
acronym = {{LFMTP}'18},
booktitle = {Proceedings of the 13th {I}nternational {W}orkshop on {L}ogical {F}rameworks and
{M}eta-{L}anguages: {T}heory and {P}ractice ({LFMTP}'18)},
author = {Rodolphe Lepigre and Christophe Raffalli},
title = {Abstract Representation of Binders in OCaml using the Bindlib Library},
pages = {42-56},
url = {https://arxiv.org/abs/1807.01872},
pdf = {https://arxiv.org/pdf/1807.01872.pdf},
doi = {10.4204/EPTCS.274.4},
abstract = {The Bindlib library for OCaml provides a set of tools for the manipulation of data structures with variable binding. It is very well suited for the representation of abstract syntax trees, and has already been used for the implementation of half a dozen languages and proof assistants (including a new version of the logical framework Dedukti). Bindlib is optimised for fast substitution, and it supports variable renaming. Since the representation of binders is based on higher-order abstract syntax, variable capture cannot arise during substitution. As a consequence, variable names are not updated at substitution time. They can however be explicitly recomputed to avoid ''visual capture'' (i.e., distinct variables with the same apparent name) when a data structure is displayed.}
}
@article{LR-toplas18,
publisher = {ACM Press},
journal = {ACM Transactions on Programming Languages and Systems},
author = {Rodolphe Lepigre and Christophe Raffalli},
title = {{Practical Subtyping for Curry-Style Languages}},
volume = {41},
number = {1},
year = {2018},
pages = {5:1--5:58},
doi = {10.1145/3285955},
pdf = {https://lepigre.fr/files/publications/LepRaf2018a.pdf},
abstract = {We present a new, syntax-directed framework for Curry-style type systems with subtyping. It supports a rich set of features, and allows for a reasonably simple theory and implementation. The system we consider has sum and product types, universal and existential quantifiers, and inductive and coinductive types. The latter two may carry size invariants that can be used to establish the termination of recursive programs. For example, the termination of quicksort can be derived by showing that partitioning a list does not increase its size. The system deals with complex programs involving mixed induction and coinduction, or even mixed polymorphism and (co-)induction. One of the key ideas is to separate the notion of size from recursion. We do not check the termination of programs directly, but rather show that their (circular) typing proofs are well-founded. Termination is then obtained using a standard (semantic) normalisation proof. To demonstrate the practicality of the system, we provide an implementation accepting all the examples discussed in the article.}
}
@inproceedings{L-types2017,
address = {Budapest, Hungary},
year = 2018,
volume = {104},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Ambrus Kaposi and Tam{\'a}s Kozsik},
acronym = {{TYPES}'17},
booktitle = {{P}roceedings of the 23rd {I}nternational {C}onference on {T}ypes for {P}roofs and {P}rograms
({TYPES}'17},
author = {Rodolphe Lepigre},
title = {{PML\(_2\):} Integrated Program Verification in ML},
pages = {4:1--4:27},
url = {http://drops.dagstuhl.de/opus/volltexte/2018/10052/},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2018/10052/pdf/LIPIcs-TYPES-2017-4.pdf},
doi = {10.4230/LIPIcs.TYPES.2017.4},
abstract = {We present the PML\(_2\) language, which provides a uniform environment for programming, and for proving properties of programs in an ML-like setting. The language is Curry-style and call-by-value, it provides a control operator (interpreted in terms of classical logic), it supports general recursion and a very general form of (implicit, non-coercive) subtyping. In the system, equational properties of programs are expressed using two new type formers, and they are proved by constructing terminating programs. Although proofs rely heavily on equational reasoning, equalities are exclusively managed by the type-checker. This means that the user only has to choose which equality to use, and not where to use it, as is usually done in mathematical proofs. In the system, writing proofs mostly amounts to applying lemmas (possibly recursive function calls), and to perform case analyses (pattern matchings).}
}
@phdthesis{Gilbert-phd2018,
author = {Gilbert, Fr{\'e}d{\'e}ric},
title = {{Extending higher-order logic with predicate subtyping}},
school = {Universit{\'e} Paris~7, Paris, France},
type = {Th{\`e}se de doctorat},
year = 2018,
month = apr,
pdf = {https://hal.inria.fr/hal-01673518/file/dissertation.pdf}
}
@mastersthesis{m2-LeenaSubramaniam,
author = {Chaitanya Leena Subramaniam},
title = {{Cubical Type Theory in Dedukti}},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = {2017},
month = sep
}
@techreport{Burel-hal18,
author = {Burel, Guillaume},
institution = {HAL Research Report},
number = {hal-01670476},
type = {Research Report},
title = {{Linking Focusing and Resolution with Selection}},
year = {2018},
month = apr,
url = {https://hal.inria.fr/hal-01670476},
pdf = {https://hal.inria.fr/hal-01670476/file/lipics.pdf},
abstract = {Focusing and selection are techniques that shrink the proof search space for respectively sequent calculi and resolution. To bring out a link between them, we generalize them both: we introduce a sequent calculus where each occurrence of an atom can have a positive or a negative polarity; and a resolution method where each literal, whatever its sign, can be selected in input clauses. We prove the equivalence between cut-free proofs in this sequent calculus and derivations of the empty clause in that resolution method. Such a generalization is not semi-complete in general, which allows us to consider complete instances that correspond to theories of any logical strength. We present three complete instances: first, our framework allows us to show that ordinary focusing corresponds to hyperresolution and semantic resolution; the second instance is deduction modulo theory and the related framework called superdeduction; and a new setting, not captured by any existing framework, extends deduction modulo theory with rewriting rules having several left-hand sides, which restricts even more the proof search space.}
}
@techreport{Thire-hal17,
author = {Thir{\'e}, Fran{\c{c}}ois},
institution = {HAL Research Report},
number = {hal-01668250},
type = {Research Report},
title = {{Exporting an Arithmetic Library from Dedukti to HOL}},
year = {2017},
month = dec,
url = {https://hal.inria.fr/hal-01668250},
pdf = {https://hal.inria.fr/hal-01668250/file/sttforall-fscd.pdf},
abstract = {Today, we observe a large diversity of proof systems. This diversity has the negative consequence that a lot of theorems are proved many times. Unlike programming languages, it is difficult for these systems to cooperate because they do not implement the same logic. Logical frameworks are a class of theorems provers that overcome this issue by their capacity of implementing various logics. In this work, we study the STT\(\forall_{\beta\delta}\) logic, an extension of the Simple Type Theory that has been encoded in the logical framework Dedukti. We show that this new logic is a good candidate to export proofs to other provers. As an example, we show how this logic has been encoded into Dedukti and how we used it to export proofs to the HOL family provers via OpenTheory.}
}
@mastersthesis{m2-genestier,
author = {Genestier, Guillaume},
title = {Termination checking in the \(\lambda\Pi\)-calculus modulo theory},
school = {Universit{\'e} Paris~7, Paris, France},
type = {Rapport de {M}aster},
year = {2017},
month = sep,
url = {https://hal.inria.fr/hal-01676409},
pdf = {https://hal.inria.fr/hal-01676409/file/Genestier_RapportLMFI.pdf}
}
@mastersthesis{m2-defourne,
author = {Defourn{\'e}, Antoine},
title = {{Proof Tactics in Dedukti}},
school = {Inria Saclay},
type = {Rapport de {M}aster},
year = {2017},
month = sep,
url = {https://hal.inria.fr/hal-01661872},
pdf = {https://hal.inria.fr/hal-01661872/file/rapport_pfe_ensimag.pdf}
}
@article{B-jfp18,
publisher = {Cambridge University Press},
journal = {Journal of Functional Programming},
author = {Blanqui, Fr{\'e}d{\'e}ric},
title = {Size-based termination of higher-order rewriting},
volume = {28},
year = {2018},
month = apr,
doi = {10.1017/S0956796818000072},
pdf = {https://hal.inria.fr/hal-01424921/file/main.pdf},
url = {https://www.cambridge.org/core/journals/journal-of-functional-programming/article/sizebased-termination-of-higherorder-rewriting/2134D9160988448FA62DD693D337892D},
abstract = {We provide a general and modular criterion for the termination of simply typed \(\lambda\)-calculus extended with function symbols defined by user-defined rewrite rules. Following a work of Hughes, Pareto and Sabry for functions defined with a fixpoint operator and pattern matching, several criteria use typing rules for bounding the height of arguments in function calls. In this paper, we extend this approach to rewriting-based function definitions and more general user-defined notions of size.}
}
@article{AM-prd17,
publisher = {American Physical Society},
journal = {Physical Review D},
author = {Arrighi, Pablo and Martiel, Simon},
title = {Quantum causal graph dynamics},
volume = {96},
number = {2},
year = {2017},
pdf = {https://arxiv.org/pdf/1607.06700.pdf},
abstract = {Consider a graph having quantum systems lying at each node. Suppose that the whole thing evolves in discrete time steps, according to a global, unitary causal operator. By causal we mean that information can only propagate at a bounded speed, with respect to the distance given by the graph. Suppose, moreover, that the graph itself is subject to the evolution, and may be driven to be in a quantum superposition of graphs—in accordance to the superposition principle. We show that these unitary causal operators must decompose as a finite-depth circuit of local unitary gates. This unifies a result on Quantum Cellular Automata with another on Reversible Causal Graph Dynamics. Along the way we formalize a notion of causality which is valid in the context of quantum superpositions of time-varying graphs, and has a number of good properties.
}
}
@book{AD18,
title = {{Le temps des algorithmes}},
author = {Abiteboul, Serge and Dowek, Gilles},
url = {https://hal.inria.fr/hal-01502505},
publisher = {{Editions Le Pommier}},
pages = {192},
year = {2017},
isbn = {978-2-7465-1175-0}
}
@inproceedings{D-PxTP17,
address = {Bras{\'{\i}}lia, Brazil},
month = sep,
year = 2017,
volume = {262},
series = {Electronic Proceedings in Theoretical Computer Science},
editor = {Catherine Dubois and Bruno {Woltzenlogel Paleo}},
acronym = {{PxTP}'17},
booktitle = {Proceedings of the 5th Workshop on Proof eXchange for Theorem Proving ({PxTP}'17)},
author = {Gilles Dowek},
title = {Analyzing Individual Proofs as the Basis of Interoperability between Proof Systems},
pages = {3-12},
url = {https://arxiv.org/abs/1712.01485v1},
pdf = {https://arxiv.org/pdf/1712.01485v1.pdf},
doi = {10.4204/EPTCS.262.1},
abstract = {We describe the first results of a project of analyzing in which theories formal proofs can be expressed. We use this analysis as the basis of interoperability between proof systems.}
}
@inproceedings{DD-tpnc17,
address = {Prague, Czech Republic},
year = 2017,
volume = 10687,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Carlos Mart{\'{\i}}n{-}Vide and
Roman Neruda and
Miguel A. Vega{-}Rodr{\'{\i}}guez},
acronym = {{TPNC}'17},
booktitle = {Proceedings of the 6th International Conference on Theory and Practice of Natural Computing ({TPNC}'17)},
author = {Alejandro D{\'{\i}}az{-}Caro and Gilles Dowek},
title = {Typing Quantum Superpositions and Measurement},
pages = {281-293},
url = {https://arxiv.org/abs/1601.04294},
doi = {10.1007/978-3-319-71069-3_22},
abstract = {We propose a way to unify two approaches of non-cloning in quantum lambda-calculi. The first approach is to forbid duplicating variables, while the second is to consider all lambda-terms as algebraic-linear functions. We illustrate this idea by defining a quantum extension of first-order simply-typed lambda-calculus, where the type is linear on superposition, while allows cloning base vectors. In addition, we provide an interpretation of the calculus where superposed types are interpreted as vector spaces and non-superposed types as their basis.}
}
@article{D-lmcs17,
journal = {Logical Methods in Computer Science},
author = {Dowek, Gilles},
title = {{Lineal: A linear-algebraic Lambda-calculus}},
volume = {13},
number = {1},
year = {2017},
month = mar,
pages = {1-33},
doi = {10.23638/LMCS-13(1:8)2017},
url = {https://lmcs.episciences.org/3203},
pdf = {https://lmcs.episciences.org/3203/pdf}
}
@article{D-flap17,
publisher = {College Publications},
journal = {IfCoLoG Journal of Logics and their Applications},
author = {Dowek, Gilles},
title = {{Rules and derivations in an elementary logic course}},
volume = {4},
number = {1},
year = {2017},
pages = {21-32},
pdf = {https://hal.inria.fr/hal-01252124/file/ttl.pdf},
note = {Special Issue: Tools for Teaching Logic}
}
@inproceedings{Genestier-hor19,
address = {Dortmund, Germany},
month = jun,
novolume = {??},
noseries = {??},
noeditor = {},
acronym = {{HOR}'19},
booktitle = {{P}roceedings of the 10th {I}nternational {W}orkshop on {H}igher-{O}rder {R}ewriting
({HOR}'19)},
author = {Genestier, Guillaume},
title = {{S}ize{C}hange{T}ool: {A} {T}ermination {C}hecker for {R}ewriting {D}ependent {T}ypes},
pages = {14--19},
year = 2019,
pdf = {https://hal.archives-ouvertes.fr/hal-02442465/file/presentationSCT.pdf}
}
@inproceedings{EBB-pxtp19,
address = {Natal, Brazil},
month = aug,
volume = {301},
series = {Electronic Proceedings in Theoretical Computer Science},
editor = {Giselle Reis and Haniel Barbosa},
acronym = {{PxTP}'19},
booktitle = {{P}roceedings of the 6th {W}orkshop on {P}roof e{X}change for {T}heorem {P}roving
({PxTP}'19)},
author = {El Haddad, Mohamed and Burel, Guillaume and Blanqui, Fr{\'e}d{\'e}ric},
title = {{E}kstrakto: {A} tool to reconstruct {D}edukti proofs from {TSTP} files (extended abstract)},
pages = {27--35},
year = 2019,
pdf = {https://hal.inria.fr/hal-02200548/file/main.pdf},
url = {http://eptcs.web.cse.unsw.edu.au/paper.cgi?PxTP2019.5}
}
@inproceedings{BGH-fscd19,
address = {Dortmund, Germany},
month = jun,
volume = {131},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Herman Geuvers},
acronym = {{FSCD}'19},
booktitle = {{P}roceedings of the 4th International Conference on
Formal Structures for Computation and Deduction ({FSCD}'19)},
author = {Fr{\'e}d{\'e}ric Blanqui and Guillaume Genestier and Olivier Hermant},
title = {Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting},
pages = {9:1-9:21},
doi = {10.4230/LIPIcs.FSCD.2019.9},
year = 2019,
pdf = {http://drops.dagstuhl.de/opus/volltexte/2019/10516/pdf/LIPIcs-FSCD-2019-9.pdf},
url = {http://drops.dagstuhl.de/opus/volltexte/2019/10516/},
abstract = {Dependency pairs are a key concept at the core of modern automated termination
provers for first-order term rewriting systems. In this paper, we introduce an extension
of this technique for a large class of dependently-typed higher-order rewriting systems.
This extends previous results by Wahlstedt on the one hand and the first author on the
other hand to strong normalization and non-orthogonal rewriting systems. This new criterion
is implemented in the type-checker Dedukti.}
}
@inproceedings{DD-fscd19,
address = {Dortmund, Germany},
month = jun,
volume = {131},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Herman Geuvers},
acronym = {{FSCD}'19},
booktitle = {{P}roceedings of the 4th International Conference on
Formal Structures for Computation and Deduction ({FSCD}'19)},
author = {Alejandro {D{\'i}az-Caro} and Gilles Dowek},
title = {Proof Normalisation in a Logic Identifying Isomorphic Propositions},
pages = {14:1-14:23},
doi = {10.4230/LIPIcs.FSCD.2019.14},
year = 2019,
pdf = {http://drops.dagstuhl.de/opus/volltexte/2019/10521/pdf/LIPIcs-FSCD-2019-14.pdf},
url = {http://drops.dagstuhl.de/opus/volltexte/2019/10521/},
abstract = {We define a fragment of propositional logic where isomorphic propositions, such
as A wedge B and B wedge A, or A ==> (B wedge C) and (A ==> B) wedge (A ==> C) are identified.
We define System I, a proof language for this logic, and prove its normalisation and consistency.}
}
@article{AMP-nc20,
publisher = {Springer},
journal = {Natural Computing},
author = {Pablo Arrighi and Simon Martiel and Simon Perdrix},
title = {{Reversible causal graph dynamics: invertibility, block representation, vertex-preservation}},
volume = {19},
number = {1},
pages = {157-178},
doi = {10.1007/s11047-019-09768-0},
year = {2020},
pdf = {https://hal.archives-ouvertes.fr/hal-02400095},
url = {https://hal.archives-ouvertes.fr/hal-02400095}
}
@inproceedings{HB-types2020,
address = {Turin, Italy},
year = 2021,
volume = {188},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Ugo de Liguoro and Stefano Berardi and Thorsten Altenkirch},
acronym = {{TYPES}'20},
booktitle = {{P}roceedings of the 26th {I}nternational {C}onference on {T}ypes for {P}roofs and {P}rograms
({TYPES}'20)},
author = {Gabriel Hondet and Fr{\'e}d{\'e}ric Blanqui},
title = {{Encoding of Predicate Subtyping with Proof Irrelevance in the $\Lambda \Pi$-Calculus Modulo Theory}},
pages = {6:1--6:18},
url = {https://drops.dagstuhl.de/opus/volltexte/2021/13885/},
pdf = {https://drops.dagstuhl.de/opus/volltexte/2021/13885/},
doi = {10.4230/LIPIcs.TYPES.2020.6}
}
@inproceedings{BM-lfmtp2020,
address = {Paris, France},
month = june,
year = 2020,
publisher = {ACM Press},
editor = {Claudio Sacerdoti Coen and Alwen Tiu},
acronym = {{LFMTP}'20},
booktitle = {Proceedings of the 15th {I}nternational {W}orkshop on {L}ogical {F}rameworks and
{M}eta-{L}anguages: {T}heory and {P}ractice ({LFMTP}'20)},
author = {Bruno Barras and Valentin Maestracci},
title = {{Implementation of Two Layers Type Theory in Dedukti and Application to Cubical Type Theory}},
pages = {54--67},
url = {https://arxiv.org/abs/2101.03810v1},
pdf = {https://arxiv.org/abs/2101.03810v1},
doi = {10.4204/EPTCS.332.4}
}
@phdthesis{thire-phd2020,
author = {Thir{\'e}, Fran{\c{c}}ois},
title = {{Meta-theory of Cumulative Types Systems and their embeddings to the $\Lambda \Pi$-calculus modulo theory}},
school = {{\'E}cole Normale Sup{\'e}rieure Paris-Saclay, France},
type = {Th{\`e}se de doctorat},
year = 2020,
month = dec,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/thire-phd20.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/thire-phd20.pdf}
}
@phdthesis{Genestier-phd2020,
author = {Genestier, Guillaume},
title = {{Dependently-Typed Termination and Embedding of Extensional Universe-Polymorphic Type Theory
using Rewriting}},
school = {{\'E}cole Normale Sup{\'e}rieure Paris-Saclay, France},
type = {Th{\`e}se de doctorat},
year = 2020,
month = dec,
opturl = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/genestier-phd20.pdf},
optpdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/genestier-phd20.pdf}
}
@article{BJO-tcs20,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Blanqui, Fr{\'{e}}d{\'{e}}ric and
Jouannaud, Jean{-}Pierre and
Okada, Mitsuhiro},
title = {Corrigendum to {\em {I}nductive-data-type systems} [Theoret. Comput. Sci.
272 {(1-2)} {(2002)} 41-68]},
volume = {817},
pages = {81--82},
doi = {10.1016/j.tcs.2018.01.010},
year = {2020},
url = {https://doi.org/10.1016/j.tcs.2018.01.010}
}
@techreport{DD-arxiv20,
author = {D{\'{\i}}az{-}Caro, Alejandro and Dowek, Gilles},
institution = {Computing Research Repository},
month = jul,
number = {2002.03762v3},
type = {Research Report},
title = {Extensional proofs in a propositional logic modulo isomorphisms},
year = {2020},
url = {https://arxiv.org/abs/2002.03762},
pdf = {https://arxiv.org/pdf/2002.03762v3.pdf}
}
@article{DDR-biosys19,
publisher = {Elsevier Science Publishers},
journal = {Biosystems},
author = {D{\'{\i}}az{-}Caro, Alejandro and Dowek, Gilles and Rinaldi, Juan Pablo},
title = {Two linearities for quantum computing in the lambda calculus},
volume = {186},
doi = {10.1016/j.biosystems.2019.104012},
year = {2019},
url = {10.1016/j.biosystems.2019.104012}
}
@inproceedings{DM-csl21,
address = {Ljubljana, Slovenia},
month = jan,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Baier, Christel and Goubault{-}Larrecq, Jean},
acronym = {{CSL}'21},
booktitle = {{P}roceedings of the 29th {A}nnual {EACSL} {C}onference on
{C}omputer {S}cience {L}ogic ({CSL}'21)},
author = {Dinis, Bruno and Miquey, {\'E}tienne},
title = {Realizability with stateful computations for nonstandard analysis},
pages = {19:1-19:23},
year = {2021},
doi = {10.4230/LIPIcs.CSL.2021.19},
pdf = {https://drops.dagstuhl.de/opus/volltexte/2021/13453/},
url = {https://drops.dagstuhl.de/opus/volltexte/2021/13453/}
}
@mastersthesis{m2-Grienenberger,
author = {Emilie Grienenberger},
title = {{Concept alignment in Logipedia - Alignement of logical connectives between HOL Light and Dedukti}},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = {2019},
month = sep
}
@phdthesis{bury-phd2019,
author = {Guillaume Bury},
title = {{Integrating rewriting, tableau and superposition into SMT}},
school = {{\'E}cole Normale Sup{\'e}rieure Paris-Saclay, France},
type = {Th{\`e}se de doctorat},
year = 2019,
month = may,
url = {https://tel.archives-ouvertes.fr/tel-02612985},
pdf = {https://tel.archives-ouvertes.fr/tel-02612985/document}
}
@article{ABF-qip20,
publisher = {Springer},
journal = {Quantum Information Processing},
author = {Pablo Arrighi and C{\'{e}}dric B{\'{e}}ny and Terry Farrelly},
title = {A quantum cellular automaton for one-dimensional {QED}},
volume = {19},
number = {88},
year = {2020},
url = {https://arxiv.org/abs/1903.07007},
doi = {10.1007/s11128-019-2555-4}
}
@article{MA-qip20,
publisher = {Springer},
journal = {Quantum Information Processing},
author = {Giuseppe Di Molfetta and Pablo Arrighi},
title = {A quantum walk with both a continuous-time limit and a continuous-spacetime limit},
volume = {19},
number = {47},
year = {2020},
url = {https://arxiv.org/abs/1906.04483},
doi = {10.1007/s11128-019-2549-2}
}
@inproceedings{Blanqui-fscd20,
address = {Paris, France},
month = jun,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Zena Ariola},
acronym = {{FSCD}'20},
booktitle = {{P}roceedings of the 5th International Conference on
Formal Structures for Computation and Deduction ({FSCD}'20)},
author = {Blanqui, Fr{\'e}d{\'e}ric},
title = {Type safety of rewriting rules in dependent types},
doi = {10.4230/LIPIcs.FSCD.2020.13},
year = 2020,
pdf = {https://drops.dagstuhl.de/opus/volltexte/2020/12335/},
url = {https://drops.dagstuhl.de/opus/volltexte/2020/12335/}
}
@inproceedings{Genestier-fscd20,
address = {Paris, France},
month = jun,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Zena Ariola},
acronym = {{FSCD}'20},
booktitle = {{P}roceedings of the 5th International Conference on
Formal Structures for Computation and Deduction ({FSCD}'20)},
author = {Genestier, Guillaume},
title = {Encoding {A}gda Programs using Rewriting},
doi = {10.4230/LIPIcs.FSCD.2020.31},
year = 2020,
pdf = {https://drops.dagstuhl.de/opus/volltexte/2020/12353/},
url = {https://drops.dagstuhl.de/opus/volltexte/2020/12353/}
}
@inproceedings{HB-fscd20,
address = {Paris, France},
month = jun,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Zena Ariola},
acronym = {{FSCD}'20},
booktitle = {{P}roceedings of the 5th International Conference on
Formal Structures for Computation and Deduction ({FSCD}'20)},
author = {Hondet, Gabriel and Blanqui, Fr{\'e}d{\'e}ric},
title = {The new rewriting engine of {D}edukti ({S}ystem {D}escription)},
pages = {35:1-35:16},
doi = {10.4230/LIPIcs.FSCD.2020.35},
year = 2020,
pdf = {https://drops.dagstuhl.de/opus/volltexte/2020/12357/},
url = {https://drops.dagstuhl.de/opus/volltexte/2020/12357/}
}
@article{JLDJ-compj20,
publisher = {Oxford University Press},
journal = {The Computer Journal},
author = {Jiang, Ying and Liu, Jian and Dowek, Gilles and Ji, Kailiang},
title = {Towards Combining Model Checking and Proof Checking},
volume = {62},
number = {9},
pages = {1365--1402},
year = 2020,
doi = {10.1093/comjnl/bxy112},
pdf = {https://hal.inria.fr/hal-01970274/file/sctl_paper.pdf}
}
@article{BBCDHH-jar20,
publisher = {Springer},
journal = {Journal of Automated Reasoning},
author = {Burel, Guillaume and Bury, Guillaume and Cauderlier, Raphaël and Delahaye, David and Halmagrand, Pierre and Hermant, Olivier},
title = {First-Order Automated Reasoning with Theories: When Deduction Modulo Theory Meets Practice},
volume = {64},
pages = {1001-1050},
year = 2020,
doi = {10.1007/s10817-019-09533-z},
pdf = {https://hal.archives-ouvertes.fr/hal-02305831/file/dmt-in-atp.pdf},
url = {https://hal.archives-ouvertes.fr/hal-02305831}
}
@inproceedings{HM-lics20,
address = {Saarbrucken, Germany},
month = jul,
publisher = {{IEEE} Press},
editor = {Kobayashi, Naoki},
acronym = {{LICS}'19},
booktitle = {{P}roceedings of the 35th {A}nnual {ACM\slash
IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'20)},
author = {Herbelin, Hugo and Miquey, {\'E}tienne},
title = {A calculus of expandable stores. {C}ontinuation-and-environment-passing style translations},
pages = {564-577},
year = 2020,
optpdf = {},
url = {https://dl.acm.org/doi/10.1145/3373718.3394792},
optdoi = {}
}
This file was generated by bibtex2html 1.98.