ITP 2017 - 8th International Conference on Interactive Theorem Proving

84 views
Skip to first unread message

jean-yves beziau

unread,
Oct 19, 2016, 2:57:15 AM10/19/16
to logi...@dimap.ufrn.br
40 macacos no PROGRAM COMITTEE !!!
Vamos torcer para que uma quantia igual ou superior de galinhas vai aparecer no evento ...
Saudações, JYB
PS What is the cost of the event, if any?

** Apologies for multiple copies, please unsubscribe *** 

                          FIRST CALL FOR PAPERS 

                                   ITP 2017 
         8th International Conference on Interactive Theorem Proving 
                               Brasilia, Brazil 
                            September 26-29, 2017 
                          http://itp2017.cic.unb.br 


Submission Deadlines: April 3, 2017 (abstracts) 
                       April 10, 2017 (full papers) 

GENERAL INFORMATION 
The ITP conference series is concerned with all topics related to 
interactive theorem proving, ranging from theoretical foundations to 
implementation aspects and applications in program verification, 
security, and formalization of mathematics. ITP is the evolution of 
the TPHOLs conference series to the broad field of interactive theorem 
proving. TPHOLs meetings took place every year from 1988 until 
2009. The eighth ITP conference, ITP 2017, will be held at 
Universidade de Brasilia, September 26-29, 2017. 

SCOPE OF CONFERENCE 
ITP welcomes submissions describing original research on all aspects 
of interactive theorem proving and its applications. Suggested topics 
include but are not limited to the following: 

*  formal aspects of hardware and software 
*  formalizations of mathematics 
*  improvements in theorem prover technology 
*  user interfaces for interactive theorem provers 
*  formalizations of computational models 
*  verification of security algorithms 
*  use of theorem provers in education 
*  industrial applications of interactive theorem provers 
*  concise and elegant worked examples of formalizations (proof pearls) 

PUBLICATION DETAILS 
The proceedings of the symposium will be published in the 
Springer's LNCS series. 

PAPER SUBMISSIONS 
All submissions must be original, unpublished, and not submitted 
concurrently for publication elsewhere. Furthermore, when appropriate, 
submissions are expected to be accompanied by verifiable evidence of 
a suitable implementation, such as the source files of a formalization 
for the proof assistant used. Submissions should be no more than 
16 pages in length and are to be submitted in PDF via EasyChair at 
the following address: 

   https://easychair.org/conferences/?conf=itp2017 

Submissions must conform to the LNCS style in LaTeX. Authors of 
accepted papers are expected to present their paper at the conference 
and will be required to sign a copyright release form. 

In addition to regular papers, described above, there will be a rough 
diamond section. Rough diamond submissions are limited to 6 pages 
and may consist of an extended abstract. They will be refereed and be 
expected to present innovative and promising ideas, possibly in an 
early form and without supporting evidence. Accepted diamonds will be 
published in the main proceedings and will be presented as short 
talks. 

IMPORTANT DATES 
Abstract submission deadline: April 3, 2017 
Full paper submission deadline: April 10, 2017 
Author notification:  June 2, 2017 
Camera-ready papers:  June 30, 2017 
Workshops & Tutorials:  September 23-25, 2017 
Conference:  September 26-29, 2017 

PROGRAM COMMITTEE 
Maria Alpuente, T.U. Valencia 
Vander Alves, U.  Brasilia 
June Andronick, U. New South Wales 
Jeremy Avigad, Carnegie Mellon U. 
Mauricio Ayala-Rincon, U. Brasilia (Co-Chair) 
Sylvie Boldo, INRIA LRI 
Ana Bove, Chalmers & Gothenburg U. 
Adam Chlipala, MIT 
Gilles Dowek, INRIA, ENS Cachan 
Aaron Dutle, NASA 
Amy Felty, U. Ottawa 
Marcelo Frias, I.T. Buenos Aires 
Ruben Gamboa, U. Wyoming 
Herman Geuvers, Radboud U. 
Elsa Gunter, U. Illinois U.C. 
John Harrison, Intel Corporation 
Nao Hirokawa, JAIST 
Matt Kaufmann, U. Texas Austin 
Mark Lawford, McMaster U. 
Andreas Lochbihler, ETH Zurich 
Assia Mahboubi, INRIA 
Panagiotis Manolios, Northeastern U. 
Cesar Munoz, NASA (Co-Chair) 
Gopalan Nadathur, U. Minnesota 
Keiko Nakata, T.U. Dresden 
Adam Naumowicz, U. Bialystok 
Tobias Nipkow, T.U. Munich 
Scott Owens, U. Kent 
Sam Owre, SRI 
Lawrence Paulson, U. Cambridge 
Leila Ribeiro, U.F.  Rio Grande do Sul 
Claudio Sacerdoti Coen, U. Bologna 
Augusto Sampaio, U.F. Pernambuco 
Monika Seisenberger, Swansea U. 
Christian Sternagel, U. Innsbruck 
Sofiene Tahar,  Concordia U. 
Woody Allen, Yuourt, U
Christian Urban, King's College London 
Josef Urban, Czech T.U. Prague 

CONTACT INFORMATION 
Cesar Munoz 
Mauricio Ayala-Rincon 
itp...@easychair.org 
http://itp2017.cic.unb.br 

-- 
Cláudia Nalon 
------------------------------------ 
Departmento de Ciência da Computação 
Instituto de Ciências Exatas 
Universidade de Brasília 
http://www.cic.unb.br/~nalon 

Valeria de Paiva

unread,
Oct 19, 2016, 1:18:59 PM10/19/16
to jean-yves beziau, Lista acadêmica brasileira dos profissionais e estudantes da área de LOGICA
Michelle Obama ja' disse que "When they go low, we go higher".
Comentarios ofensivos no nivel de escola primaria (ou do "locker room do Trump") nao precisam e nao deviam aparecer na lista de logica, com ou sem o pretexto de um senso de humor "excentrico".

Acho que esta na hora dos nossos colegas se manifestarem contra esse tipo de "brincadeira" ofensiva e sexista.

Valeria


On Tue, Oct 18, 2016 at 5:22 PM, jean-yves beziau <jyb.lo...@gmail.com> wrote:
40 macacos no PROGRAM COMITTEE !!!
Vamos torcer para que haja uma quantia igual ou superior de galinhas no evento ...
Saudações, JYB
Woody Allen, Cumy. New OrQ

Christian Urban, King's College London 
Josef Urban, Czech T.U. Prague 

CONTACT INFORMATION 
Cesar Munoz 
Mauricio Ayala-Rincon 
itp...@easychair.org 
http://itp2017.cic.unb.br 

-- 
Cláudia Nalon 
------------------------------------ 
Departmento de Ciência da Computação 
Instituto de Ciências Exatas 
Universidade de Brasília 
http://www.cic.unb.br/~nalon 

jean-yves beziau

unread,
Oct 20, 2016, 12:45:02 PM10/20/16
to logi...@dimap.ufrn.br
Cara Valeria

Concordo plenamente: deveriamos prohibir este Biziou de interferir nesta lista, assim que outros lógicos franceses cuja reputação ja é seriamante comprometida:

O Bruno Poizat publicou um livro sobre teoria da estabilidade cheio de fotos de mulher peladas, foi publicado em ingles no Estados Unidos mas felizemente tirar as fotos!
Bruno Poizat, Groupes stables
http://www.ams.org/books/surv/087/surv087-endmatter.pdf
O Ruy de Queiroz tem intenção de publicar este livro no Brasil, espero que ele siga o mesmo procedimento ou talvez pode simplesemente, usando photoshop, acrescentar roupas acima dessas mulheres.

Outro logico frances doido é o:
Jean-Yves Girard
sem comentarios!!!

Para acabar com essa bagunça, suggero então excluir esses rapazes da lista, 
tenho uma suggestão para a comissao de censura da lista logica-l:
em vez de puremente e simplesemente prohibir a entrada deles
poderia botar um programa  para filtrar as entradas 
uma versão intelligente do Capcha que eu fiquei desenvolvendo com a  equipe de Intelligence Artificial  da CIA baseada na logica paraconsistente tubopolar versao 3.14
Veja aqui:
Acredito então que so uma pessoa que tem um QI superior a Beta 1 pode conseguir a passar este teste, certamente o Biziou nao vai passar. Uma maneira entao bastante elegante de filtrar a lista!

Para finalizar, alem de trabalhar com a CIA eu colobaro também com o Kagibi.
Veja aqui a foto que o Kagibi fiz recetemente do Biziou :
Ele esta complotando com a Vicky Popov, uma gata da Siberia que escapou do campo Goulash 431 de Novousibirka e que esta procurada pelo Kagibi ha varios anos.
Mantarei voce informado sobre a  evoluação da situação

No aguardo estou mandando uma video que acabei de gravar (além de ensinar a lógica, também eu canto ...),
eu mesmo fiz a composição da letras:

Pedro Lifero

Date: 2016-10-19 19:18 GMT+02:00
Subject: [META] Re: ITP 2017 - 8th International Conference on Interactive Theorem Proving
To: jean-yves beziau <jyb.lo...@gmail.com>
Cc: Lista acadêmica brasileira dos profissionais e estudantes da área de LOGICA <logi...@dimap.ufrn.br>

Rodrigo Podiacki

unread,
Oct 20, 2016, 12:53:39 PM10/20/16
to Lista acadêmica brasileira dos profissionais e estudantes da área de LOGICA
Valeria,

Me pergunto por que ele não escreve assim na FOM.

--
Você recebeu essa mensagem porque está inscrito no grupo "LOGICA-L" dos Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+unsubscribe@dimap.ufrn.br.
Para postar nesse grupo, envie um e-mail para logi...@dimap.ufrn.br.
Acesse esse grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
 Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAF2zFLCbFUS78sE3MytmkdGFD3ExPU11LvcDCZXnvRicpdm_Mw%40mail.gmail.com.

Joao Marcos

unread,
Oct 20, 2016, 1:05:30 PM10/20/16
to Lista acadêmica brasileira dos profissionais e estudantes da área de LOGICA
> Me pergunto por que ele não escreve assim na FOM.

Uma pergunta retórica, claro.

Já eu me pergunto que interesse poderíamos ter em alimentar um thread
claramente OFF-TOPIC que só alegra aqueles que se esforçam por causar
impressão, em afronta à "political correctness" (e ao _bom gosto_):
https://groups.google.com/a/dimap.ufrn.br/forum/#!searchin/logica-l/political$20correctness

As novas *regras de convívio* da lista deixam bem claro o que
esperamos do comportamento dos membros (todos os membros) desta lista:
https://docs.google.com/document/d/1nXljf_KASE8xIY9Vh8rrlTAPwZ7X9HnEzjTRNM7hWe4/edit

Esta é minha última mensagem sobre este assunto.
Joao Marcos
>> um e-mail para logica-l+u...@dimap.ufrn.br.
>> Para postar nesse grupo, envie um e-mail para logi...@dimap.ufrn.br.
>> Acesse esse grupo em
>> https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
>> Para ver essa discussão na Web, acesse
>> https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAF2zFLCbFUS78sE3MytmkdGFD3ExPU11LvcDCZXnvRicpdm_Mw%40mail.gmail.com.
>
>
> --
> Você recebeu essa mensagem porque está inscrito no grupo "LOGICA-L" dos
> Grupos do Google.
> Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie
> um e-mail para logica-l+u...@dimap.ufrn.br.
> Para postar nesse grupo, envie um e-mail para logi...@dimap.ufrn.br.
> Acesse esse grupo em
> https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
> Para ver essa discussão na Web, acesse
> https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAE9%3DZVxmMQyhDf8r976WoPvTrqm1iKZyK16ux1jLMobuECwN6w%40mail.gmail.com.



--
http://sequiturquodlibet.googlepages.com/

Marcos Silva

unread,
Oct 20, 2016, 9:40:39 PM10/20/16
to logical logical
Caros colegas,

eu, como negro e professor de alguns alunos negros, gostaria de manifestar meu repúdio à mensagem do colega Jean-Yves Beziau.

Me solidarizo com as preocupações da colega Valéria de Paiva em seu protesto solitário (e corajoso).

++++

Em emails privados, tentei, cordialmente, esclarecer ao JY Beziau o quanto pode ser ofensivo os usos de "macaco" e "galinha" no Brasil. 

Ele me pareceu, também cordialmente, não entender (ou não querer entender) este fato. De toda forma, acho uma falta de respeito com os costumes e história (muito dura!) de um país que o acolheu com tanta generosidade.

Dado o seu papel institucional em sociedades como a Brasileira de Lógica e como professor e orientador de jovens em uma instituição muito importante como a UFRJ, lamento que JY, com tantos trabalhos brilhantes, se comporte desta maneira em uma lista pública com centenas de membros.

++++

Também gostaria de manifestar o meu grande descontentamento, e acho que não sou o único, com a negligência da administração desta lista, ao longo dos últimos anos, com reiterados comentários sexistas e racistas de alguns de seus membros (ilustres). 

Torço que a nova administradora, Carolina Blasio, não repita esta estratégia nociva de permissividade. 

Eu realmente achava que se deveria ter algum dispositivo para que um infeliz email, como o enviado pelo JY Beziau no dia 18/10, não chegasse a tantas pessoas interessadas em discutir e divulgar assuntos relacionados à lógica.

++++

Em alguns casos importantes, ignorar significa (politicamente) consentir.  




>> Para postar nesse grupo, envie um e-mail para logi...@dimap.ufrn.br.
>> Acesse esse grupo em
>> https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
>> Para ver essa discussão na Web, acesse
>> https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAF2zFLCbFUS78sE3MytmkdGFD3ExPU11LvcDCZXnvRicpdm_Mw%40mail.gmail.com.
>
>
> --
> Você recebeu essa mensagem porque está inscrito no grupo "LOGICA-L" dos
> Grupos do Google.
> Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie
--
http://sequiturquodlibet.googlepages.com/

--
Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+unsubscribe@dimap.ufrn.br.
Para postar neste grupo, envie um e-mail para logi...@dimap.ufrn.br.
Visite este grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAO6j_LiyhG0dt3d3P%2BiNQg3e4%2BG8Mp3WcquQ6mTXZ5hEQ_20gg%40mail.gmail.com.



--
Marcos Silva
Philosophie macht Spaß!

Administradores LOGICA-L

unread,
Oct 21, 2016, 3:59:13 AM10/21/16
to logi...@dimap.ufrn.br
Caros participantes da Logica-L,

A Logica-L é um espaço para discussão e divulgação de lógica e estou trabalhado de acordo com as regras de convívio, criadas pelos próprios participantes da lista, para que as mensagens nela postadas não fujam a este escopo.

Devo lembrar que um longo debate já foi realizado nesta lista em relação a adoção ou não da moderação e a decisão coletiva foi evitá-la. Como administradora minha postura será sempre permitir a liberdade de expressão e manter o registro perene e público do que for aqui escrito dando, assim, a oportunidade para que cada um seja o próprio responsável de seus atos. "scripta manente".

Peço para que esta thread seja encerrada por aqui pois ela já foi muito além do assunto que a lista se propõe. Nada impede, contudo, que o que aqui está registrado seja assunto em outros espaços de discussão (virtuais ou não).

Agradeço a atenção e colaboração de todos,

Carolina
Administradora da Logica-L


>> um e-mail para logica-l+u...@dimap.ufrn.br.

>> Para postar nesse grupo, envie um e-mail para logi...@dimap.ufrn.br.
>> Acesse esse grupo em
>> https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
>> Para ver essa discussão na Web, acesse
>> https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAF2zFLCbFUS78sE3MytmkdGFD3ExPU11LvcDCZXnvRicpdm_Mw%40mail.gmail.com.
>
>
> --
> Você recebeu essa mensagem porque está inscrito no grupo "LOGICA-L" dos
> Grupos do Google.
> Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie
> um e-mail para logica-l+u...@dimap.ufrn.br.
--
http://sequiturquodlibet.googlepages.com/

--
Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+u...@dimap.ufrn.br.
--
Marcos Silva
Philosophie macht Spaß!

--
Você recebeu essa mensagem porque está inscrito no grupo "LOGICA-L" dos Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+unsubscribe@dimap.ufrn.br.
Para postar nesse grupo, envie um e-mail para logi...@dimap.ufrn.br.
Acesse esse grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAGZ3pz%2Bv1SzX_RCpdM8hzW5rYDzGiS-dGVtBr4K-84xE07D-wQ%40mail.gmail.com.

Reply all
Reply to author
Forward
0 new messages