The Coq mailing list

[Pierre Corbineau <corbinea AT lri.fr>]

========================================================================

                          CALL FOR PARTICIPATION
                            CHIT/CHAT Workshop

                  Curry-Howard Implementation techniques 
                                    /
                    Connecting Humans and Typecheckers
       
                      http://www.cs.ru.nl/chitchat/
        This is a Small Workshop of the European TYPES IST Action.
                  Nijmegen (Netherlands), 18-22 December 2006  

The CHIT Workshop aims at gathering implementers of Curry-Howard based
Theorem provers/Programming environments to discuss implementation
issues. Its aim is to share isolated experience of development teams
of those systems. We especially welcome implementers from new systems
to participate.

The CHAT Workshop focusses on interaction between users and proof
environments, graphical interfaces, and network-based interaction.

Important Dates:

- Friday 18 November 2006: Abstract submission

I - Curry-Howard Implementation Techniques (CHIT)

   18-20 December 2006

Keywords:

    -  Terms and binders
    -  Type inference, type constraints and unification
    -  Reduction, evaluation and compilation
    -  Proof refinement/Proof engine
    -  State handling, library, saving ...
    -  Coercions
    -  Termination checking

Morning Sessions will be held by key implementers of the Systems, and be
focussed on specific features. Other participants may propose short talks,
however, we want to reserve much time for discussions and hacking sessions. 
Time will be alloted for discussions about perspectives and collected
experience, and also about challenges for the future. 

II - Connecting Humans And Typecheckers (CHAT)

   21-22 December 2006

Keywords:

    -  Declarative versus procedural proof styles (structured proofs, XML)
    -  Web based interfaces (including cooperative environments)
    -  Libraries and information retrieval (including search engines)
    -  Proof documentation (literate proving)
    -  Protocols for UI-interaction

The CHAT workshop will focus on interaction between users and proof
environments, graphical interfaces, and on network-based interaction.
Participants are welcome to submit short talks about the above
subjects.

To register and/or submit talks, please go to the web page at:
          http://www.cs.ru.nl/chitchat/


Contact: 
typeschitchat AT cs.ru.nl


Organizing Commitee:

Pierre Corbineau
Bas Spitters
Cezary Kaliszyk 
Herman Geuvers

==========================================================================