All Slimmer related publications

David Baelde.
A linear approach to the prooftheory of least and greatest
fixed points.
PhD thesis, Ecole Polytechnique, December 2008.
[ bib 
http ]

David Baelde.
On the expressivity of minimal generic quantification.
In A. Abel and C. Urban, editors, International Workshop on
Logical Frameworks and MetaLanguages: Theory and Practice (LFMTP 2008),
number 228 in ENTCS, pages 319, 2008.
[ bib 
http ]

David Baelde.
On the proof theory of regular fixed points.
In Martin Giese and Arild Waller, editors, TABLEAUX 09:
Automated Reasoning with Analytic Tableaux and Related Methods, number 5607
in LNAI, pages 93107, 2009.
[ bib 
.pdf ]

David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, and Alwen Tiu.
A User Guide to Bedwyr, November 2006.
[ bib 
.pdf ]

David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, and Alwen Tiu.
The Bedwyr system for model checking over syntactic expressions.
In F. Pfenning, editor, 21th Conf. on Automated Deduction
(CADE), number 4603 in LNAI, pages 391397. Springer, 2007.
[ bib 
.pdf ]

David Baelde and Dale Miller.
Least and greatest fixed points in linear logic.
In N. Dershowitz and A. Voronkov, editors, International
Conference on Logic for Programming and Automated Reasoning (LPAR), volume
4790 of LNCS, pages 92106, 2007.
[ bib 
.pdf ]

David Baelde and Dale Miller.
Least and greatest fixed points in linear logic: extended version.
Technical report, available from the first author's web page, April
2007.
[ bib 
.pdf ]

David Baelde, Dale Miller, and Zachary Snow.
Focused inductive theorem proving.
In J. Giesl and R. Hähnle, editors, Fifth International
Joint Conference on Automated Reasoning, number 6173 in LNCS, pages
278292, 2010.
[ bib 
.pdf ]

Andrew Gacek.
Relating nominal and higherorder abstract syntax specifications.
In Proceedings of the 2010 Symposium on Principles and Practice
of Declarative Programming, pages 177186. ACM, July 2010.
[ bib 
.pdf ]

Andrew Gacek, Dale Miller, and Gopalan Nadathur.
Combining generic judgments with recursive definitions.
In F. Pfenning, editor, 23th Symp. on Logic in Computer
Science, pages 3344. IEEE Computer Society Press, 2008.
[ bib 
.pdf ]

Andrew Gacek, Dale Miller, and Gopalan Nadathur.
Reasoning in Abella about structural operational semantics
specifications.
In A. Abel and C. Urban, editors, International Workshop on
Logical Frameworks and MetaLanguages: Theory and Practice (LFMTP 2008),
number 228 in ENTCS, pages 85100, 2008.
[ bib 
http 
.pdf ]

Andrew Gacek, Dale Miller, and Gopalan Nadathur.
Nominal abstraction.
Extended version of LICS 2008 paper. Accepted to Information and
Computation, September 2010.
[ bib 
http ]

Andrew Gacek, Dale Miller, and Gopalan Nadathur.
A twolevel logic approach to reasoning about computations.
Accepted to the J. of Automated Reasoning, August 2010.
[ bib 
http ]

Chuck Liang and Dale Miller.
Focusing and polarization in intuitionistic logic.
In J. Duparc and T. A. Henzinger, editors, CSL 2007: Computer
Science Logic, volume 4646 of LNCS, pages 451465. Springer, 2007.
[ bib 
.pdf ]

Chuck Liang and Dale Miller.
On focusing and polarities in linear logic and intuitionistic logic.
Extended version of accepted paper., September 2007.
[ bib 
http 
.pdf ]

Chuck Liang and Dale Miller.
Focusing and polarization in linear, intuitionistic, and classical
logics.
Theoretical Computer Science, 410(46):47474768, 2009.
[ bib 
http ]

Chuck Liang and Dale Miller.
A unified sequent calculus for focused proofs.
In LICS: 24th Symp. on Logic in Computer Science, pages
355364, 2009.
[ bib 
.pdf ]

Dale Miller.
Representing and reasoning with operational semantics.
In U. Furbach and N. Shankar, editors, Proceedings of IJCAR:
International Joint Conference on Automated Reasoning, volume 4130 of
LNAI, pages 420, August 2006.
[ bib 
.dvi 
.pdf ]

Dale Miller.
Formalizing operational semantic specifications in logic.
Concurrency Column of the Bulletin of the EATCS, October 2008.
[ bib 
.pdf ]

Dale Miller.
Formalizing operational semantic specifications in logic.
In Proceedings of the 17th International Workshop on Functional
and (Constraint) Logic Programming (WFLP 2008), volume 246, pages 147165,
August 2009.
[ bib 
http ]

Dale Miller.
Reasoning about computations using twolevels of logic.
In K. Ueda, editor, Proceedings of the 8th Asian Symposium
on Programming Languages and Systems (APLAS'10), number 6461 in
LNCS, pages 3446, 2010.
[ bib 
.pdf ]

Dale Miller and Vivek Nigam.
Incorporating tables into proofs.
In J. Duparc and T. A. Henzinger, editors, CSL 2007: Computer
Science Logic, volume 4646 of LNCS, pages 466480. Springer, 2007.
[ bib 
.pdf ]

Dale Miller and Alexis Saurin.
A game semantics for proof search: Preliminary results.
In Proceedings of the Mathematical Foundations of Programming
Semantics (MFPS05), number 155 in ENTCS, pages 543563, 2006.
[ bib 
.pdf ]

Dale Miller and Alexis Saurin.
From proofs to focused proofs: a modular proof of focalization in
linear logic.
In J. Duparc and T. A. Henzinger, editors, CSL 2007: Computer
Science Logic, volume 4646 of LNCS, pages 405419. Springer, 2007.
[ bib 
.pdf ]

Alberto Momigliano and Alwen Tiu.
Induction and coinduction in sequent calculus.
In Mario Coppo, Stefano Berardi, and Ferruccio Damiani, editors,
Postproceedings of TYPES 2003, number 3085 in LNCS, pages 293308, January
2003.
[ bib 
.pdf ]

Elaine Pimentel and Dale Miller.
On the specification of sequent systems.
In LPAR 2005: 12th International Conference on Logic for
Programming, Artificial Intelligence and Reasoning, number 3835 in LNAI,
pages 352366, 2005.
[ bib 
.pdf ]

Alexis Saurin.
Separation with streams in the λμcalculus.
In 20th IEEE Symposium on Logic in Computer Science (LICS
2005), pages 356365. IEEE Computer Society, 2005.
[ bib ]

Alwen Tiu and Dale Miller.
Proof search specifications of bisimulation and modal logics for the
πcalculus.
ACM Trans. on Computational Logic, 11(2), 2010.
[ bib 
http ]

Alwen Tiu, Gopalan Nadathur, and Dale Miller.
Mixing finite success and finite failure in an automated prover.
In Empirically Successful Automated Reasoning in HigherOrder
Logics (ESHOL'05), pages 7998, December 2005.
[ bib 
.pdf ]