The Coq mailing list

[Gopalan Nadathur <gopalan AT cs.umn.edu>]

[I am addressing this message also to the mailing list since the information may be of interest to others.]

Dear Christophe,

Here is what we say related to your question in the introduction:

--------------------------------------------------
The ideal reader of this book would have had prior exposure to high-level
programming and to the rudiments of logic and logic programming.  We 
specifically assume that the reader knows how to write and execute 
simple programs in some dialect of Prolog. ... Knowledge of ``advanced'' 
aspects of Prolog, however, is not necessary. In fact, such knowledge 
could be confusing: advanced Prolog features often derive from non-logical 
aspects of the language whereas our focus here will be on finding logical 
solutions to the problems that have led to the proliferation of non-logical
solutions that are familiar to Prolog programmers.
---------------------------------------------------

On the logic side, what is needed is mainly a predisposition to presentations 
like the sequent calculus and to computational aspects such as unification.
Most of what is actually needed is developed in the book.

Hope this helps.

Regards,
-Gopalan

On Fri, Sep 7, 2012 at 3:57 PM, Christophe BAL <projetmbc AT gmail.com> wrote:
> Hello,
> can you indicate the minimal knowledge needed to read your book ?
>
> Thanks.
> Christophe.
>
>
> 2012/9/7 Gopalan Nadathur <gopalan AT cs.umn.edu>
>>
>> Dale Miller and I are happy to announce the recent publication of our
>> book entitled "Programming with Higher-Order Logic" by Cambridge
>> University Press. The table of contents and other details about the
>> book can be found at https://sites.google.com/site/proghol/.
>>
>> The book argues for using higher-order intuitionistic logic as the
>> foundations of logic programming. In elaborating this argument, the
>> book presents
>>   - a sequent calculus based characterization of logic programming;
>>   - a proof search approach to computation;
>>   - higher-order logic programming;
>>   - polymorphic typing;
>>   - modular programming and abstract data types; and
>>   - simply-typed lambda-terms and their unification.
>>
>> The book also emphasizes the practical application of higher-order
>> logic programming by showing that it can be used to provide elegant
>> formalizations and implementations of computations that manipulate
>> bindings in syntax.  In addition to a general exposition of this
>> approach, individual chapters present extended examples relating to
>>   - implementing proof systems,
>>   - computing with functional programs, and
>>   - encoding the pi-calculus.
>>
>> The lambda Prolog language is used to illustrate the underlying
>> computation-related ideas and their applications. The website for the
>> book provides all the lambda Prolog code used in the book. The reader
>> can experiment with this code using the Teyjus system available from
>> http://teyjus.cs.umn.edu/.
>
>