Profile

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

Stream

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...
 
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...

Dale Miller

Shared publicly  - 
 
The text of Snowden's Testimony To European Parliament.  Strongly recommended.
1
2
Giuseppe Primiero's profile photoHeinrich C. Kuhn's profile photo
Add a comment...
Have him in circles
212 people
Степанов Аванев's profile photo
Adriana Compagnoni's profile photo
Helmut Veith's profile photo
Marie Antoinette LeDonne's profile photo
Luke Ong's profile photo
Danko Ilik's profile photo
Sidiki Kabré's profile photo
Rob Simmons's profile photo
Marina Correia's profile photo

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.
11 comments on original post
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...

Dale Miller

Shared publicly  - 
 
Here's an awkward question that may be urgent: Are we getting over 9.11? Will we ever? Do we want to? Is it a scar by now, or a wound still bleeding? Is it a post-traumatic-stress disorder? What is it doing to our character, our culture, our Constitution? After a monstrous attack on the American ...
1
Add a comment...
People
Have him in circles
212 people
Степанов Аванев's profile photo
Adriana Compagnoni's profile photo
Helmut Veith's profile photo
Marie Antoinette LeDonne's profile photo
Luke Ong's profile photo
Danko Ilik's profile photo
Sidiki Kabré's profile photo
Rob Simmons's profile photo
Marina Correia'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