Profile

Cover photo
Dale Miller
Works at INRIA & LIX/Ecole Polytechnique
Attended Carnegie Mellon University
Lives in Orsay, France
226 followers|192,075 views
AboutPostsPhotos+1's

Stream

Dale Miller

Shared publicly  - 
 
One or two postdoctoral positions are available from Inria-Saclay within the LIX laboratory of Ecole Polytechnique.  These positions are
supported by the ERC Advanced Grant ProofCert and are part of a long-term effort to build trustable proof checkers for a wide variety of proof structures.
1
1
Giuseppe Primiero's profile photo
Add a comment...

Dale Miller

Shared publicly  - 
 
A new tutorial on how to use the Abella interactive theorem prover is available from the Journal of Formalized Reasoning.  

``Abella: A System for Reasoning about Relational Specifications'' by David Baelde, Kaustuv Chaudhuri, Andrew Gacek, Dale iller, Gopalan Nadathur, Alwen Tiu, and Yuting Wang

This prover reasons directly with inductively and co-inductively defined relations (instead of functions).  Particularly novel features of Abella include its support for lambda-tree syntax, the nabla-quantifier, and the two-level logic approach to reasoning with logic specifications.
The journal is meant to become the natural
4
1
Jan Burse's profile photo
Add a comment...

Dale Miller

Shared publicly  - 
 
@Maclomaclee looks a bit like Fig 7 in bit.ly/1qYfz6A · 27 minutes ago. You must listen to BBC R4 Soul Music, on La Bohème bbc.in/1wbjhhR (and see bit.ly/1wbjeCu ). 35 minutes ago · @Maclomaclee CL are just another way of expressing P values, so suffer from the same problems ...
1
Add a comment...

Dale Miller

Shared publicly  - 
 
The call-for-papers for the 42nd International Colloquium on Automata, Languages, and Programming (ICALP 2015) is now on line.  The meeting will take place in Kyoto, Japan during 6-10 July 2015.
1
Add a comment...

Dale Miller

Shared publicly  - 
 
The Tour de France has just moved through Orsay.
3
Add a comment...

Dale Miller

Shared publicly  - 
 
The ACM Special Interest Group on Logic and Computation (SIGLOG) is now open for membership.
The ACM Special Interest Group on Logic and Computation (SIGLOG) is a community organization dedicated to the advancement of logic and computation, and formal methods in Computer Science, broadly defined. SIGLOG aims to serve a broad range of interests. The flagship conference will be the ...
6
6
Andre Platzer's profile photoFederico Gobbo's profile photo
Add a comment...

Dale Miller

Shared publicly  - 
 
The Vienna Summer of Logic should be the largest event in the history of logic.  The call for volunteers to help with this meeting is now open.  In 1983, I volunteered for a meeting on the lambda-calculus and functional programming and I was able to meet Church, Curry, and Rosser among others giants of the field.   I'm sure that this summer's meeting will offer young attendees similar opportunities.
3
Add a comment...
In his circles
411 people
Have him in circles
226 people
Viktor Trautwain's profile photo
yannick le thiec's profile photo
Ali Malik's profile photo
Chandradath Baboolal's profile photo
Katelyn Warren's profile photo
Anupam Das's profile photo
Matthias Puech's profile photo
Lola Kovacic's profile photo
Calendrier VIP's profile photo

Dale Miller

Shared publicly  - 
 
I gave a CS Department Colloquium on "Communicating and trusting formal proofs" at ETH Zurich on 20 April.  You can find the slides and audio of this talk as a video on their multimedia portal.

Abstract:  In the mist of feeling insecure with our electronic communications, we can take solace in the advice that we can "trust the math" behind cryptography.  Faced with concerns over the safety of fly-by-wire planes and self-driving cars, we should be able to find solace in the fact that some parts of our safety critical systems have been proved formally correct: that is, we should be able to "trust the proof".  The way formal proofs are built today, however, makes trusting them difficult.  While proof assistants are used to build formal proofs, those proofs are often locked to that assistant. Formal proofs produced by one proof assistant cannot usually be checked and trusted by another proof assistant nor by a future version of itself.  Thus, one of the components of the scientific method that ensures trust---reproducibility---is missing from proof checking.

The field of proof theory, as initiated by Gentzen in the 1930's, has identified a great deal of structure in formal proofs.  Given recent developments in this topic, it is now possible to apply what we know about proofs in theory to what we would like to have for proofs in practice.  To that end, I will present the Foundational Proof Certificates framework for defining the semantics of proof evidence. Since such definitions are executable, it is possible to build proof checkers that can check a wide range of formal proofs.  In this scheme, the logic engine that executes such definitions is the only thing that needs to be trusted.  Since such a logic engine is based on well-known computational logic topics, anyone can write a logic engine in their choice of programming language and hardware in order for them to build a checker they can trust.  I will also overview some of the consequences of defining proofs in this manner: provers can become networked far more richly than they are currently and both libraries and marketplaces of proofs are enabled in a technology independent fashion.
2
3
Philip Thrift's profile photoWilliam Rutiser's profile photo
Add a comment...

Dale Miller

Shared publicly  - 
Cory Doctorow on why privacy is about more than concealing crime—and why backdoors are inevitably available to everyone, not just people you trust.
1
Add a comment...

Dale Miller

Shared publicly  - 
 
 
Tom Ball, Ras Bodik, +Greg Morrisett, and I are organizing a new kind of programming languages conference. We already have several excellent conferences, but they are focused on incremental bits of novelty. We want to create a new kind of venue that complements these: to present and discuss big-picture questions and long-running programs; to view progress along the long arc of a research effort. The conference is May 3-6, 2015 in lovely Asilomar (on the Pacific Coast), CA, USA.

If this sounds interesting, please: don't just +1 it, reshare it. Why? To keep costs down and retain ownership of the conference with the community, we are independent, not affiliated with any organizations. That means you are the only PR channel we have. So please do us a favor. Thanks.
1
2
Sylvain Soliman's profile photoClément Houtmann's profile photo
Add a comment...

Dale Miller

Shared publicly  - 
 
It's time to register for the Vienna Summer of Logic, July 9-24, 2014.
http://vsl2014.logic.at 
1
1
Giuseppe Primiero's profile photo
Add a comment...

Dale Miller

Shared publicly  - 
 
I am looking for two PhD students and two post doc to start in Fall 2014. 
1
4
V Stolz's profile photoMelanie Courtot's profile photo
Add a comment...
People
In his circles
411 people
Have him in circles
226 people
Viktor Trautwain's profile photo
yannick le thiec's profile photo
Ali Malik's profile photo
Chandradath Baboolal's profile photo
Katelyn Warren's profile photo
Anupam Das's profile photo
Matthias Puech's profile photo
Lola Kovacic's profile photo
Calendrier VIP's profile photo
Work
Occupation
Director of Research
Employment
  • INRIA & LIX/Ecole Polytechnique
    Director of Research, present
  • University of Pennsylvania, Penn State, INRIA, Ecole Polytechnique
Places
Map of the places this user has livedMap of the places this user has livedMap of the places this user has lived
Currently
Orsay, France
Previously
Annville, Pennsylvania, USA - Nervi, Genoa, Italy - Edinburgh, Scotland - Boalsburg, PA, USA - Pittsburgh, PA, USA - Philadelphia. PA, USA
Story
Introduction
Raised in Annville, Pennsylvania.  Undergraduate studies at Lebanon Valley College. Graduate studies at Carnegie Mellon University.  Fourteen years on the faculty of the University of Pennsylvania and five years on the faculty of Penn State.  Since 2002, Director of Research at INRIA Saclay & LIX/Ecole Polytechnique, outside Paris, France.
Education
  • Carnegie Mellon University
    Mathematics, 1978 - 1983
  • Lebanon Valley College
    Mathematics, 1974 - 1978
Basic Information
Gender
Male
Dale Miller's +1's are the things they like, agree with, or want to recommend.
Polarity in Type Theory
existentialtype.wordpress.com

There has recently arisen some misguided claims about a supposed opposition between functional and object-oriented programming. The claims a

Abella
abella.cs.umn.edu

Description. Abella is an interactive theorem prover based on lambda-tree syntax. This means that Abella is well-suited for reasoning about

Gopalan Nadathur
www.cs.umn.edu

Contents. Research Interests and Activities; My Research Papers; Some Recent Talks; Teyjus--A Lambda Prolog Implementation; Conference Progr

Bedwyr
slimmer.gforge.inria.fr

Bedwyr: A proof search approach to model checking. Overview. Bedwyr is a generalization of logic programming that allows model checking dire

λProlog - Wikipedia, the free encyclopedia
en.wikipedia.org

λProlog. From Wikipedia, the free encyclopedia. Jump to: navigation, search. λProlog, also written lambda Prolog, is a logic programming lan

Dale Miller
www.lix.polytechnique.fr

Home page for Dale Miller

Bienvenue dans l'igloo de mrpingouin!
www.lix.polytechnique.fr

David Baelde. I'm a computer science researcher. I'm generally interested in the foundations of logics and programming. I work mostl

ProofCert » Parsifal
team.inria.fr

ProofCert: Broad Spectrum Proof Certificates. ProofCert is the name of an ERC Advanced Grant awarded to Dale Miller for the five years 2012-

Parsifal »
team.inria.fr

Preuves Automatiques et Raisonnement sur des SpécIFicAtions Logiques. Parsifal has been a team within LIX since September 2003 and an INRIA

Travelling Salesman Movie
www.travellingsalesmanmovie.com

Watch the Travelling Salesman HD trailer.

CPP 2012
cpp12.kuis.kyoto-u.ac.jp

The CPP and APLAS meetings will share two keynote speakers. We are delighted that. Xavier Leroy, INRIA and; Greg Morrisett, Harvard Universi

NASA - Opportunity's Selfie
www.nasa.gov

NASA's Mars Rover Opportunity catches its own late-afternoon shadow in this dramatically lit view eastward across Endeavour Crater on Mars.

A CS Professor's blog: Harvard: a model for French universities?
teachingintrotocs.blogspot.com

Yesterday's issue of Le Monde newspaper had a full page article on everything that is admirable about Harvard, the "best university

Papers and Talks of Dale Miller
www.lix.polytechnique.fr

A Proof-Theoretic Approach to the Static Analysis of Logic Programs by Dale Miller. In Reasoning in Simple Type Theory: Festschrift in honou

Pisa Summer Workshop on Proof Theory
www.helsinki.fi

[Arno]. Pisa Summer Workshop on Proof Theory. Pisa, Italy, 12-15 June 2012. Organizers: Department of Philosophy, University of Pisa; Depart

Andrew Gacek
www.cs.umn.edu

I'm the one in the middle :-). Andrew Gacek. Department of Computer Science and Engineering. Institute of Technology. University of Minn

Home Page | CPP 2011
formes.asia

First International Conference on. Certified Programs and Proofs. (CPP 2011). December 7–9, 2011, Taiwan. http://formes.asia/cpp. (co-locate

Catuscia Palamidessi's home page
www.lix.polytechnique.fr

INRIA Saclay and LIX LIX, École Polytechnique, Rue de Saclay, 91128 Palaiseau Cedex, FRANCE Office: +33 (0)1 69 33 41 17 Assistant: +33 (0)1

λProlog Home Page
www.lix.polytechnique.fr

λProlog. Programming with higher-order logic. λProlog is a logic programming language based on an intuitionistic fragment of Church's Si