| |
|
|
|
|
|
|
|
|
1. |
Record Nr. |
UNINA9910557461103321 |
|
|
Autore |
Chlipala Adam <1981-> |
|
|
Titolo |
Certified programming with dependent types : a pragmatic introduction to the Coq proof assistant / / Adam Chlipala |
|
|
|
|
|
|
|
Pubbl/distr/stampa |
|
|
Cambridge, : The MIT Press, 2013 |
|
Cambridge, Massachusetts : , : MIT Press, , [2013] |
|
[Piscataqay, New Jersey] : , : IEEE Xplore, , [2013] |
|
|
|
|
|
|
|
|
|
Descrizione fisica |
|
|
|
|
|
|
Collana |
|
|
|
|
|
|
Disciplina |
|
|
|
|
|
|
Soggetti |
|
Automatic theorem proving - Computer programs |
Computer programming |
|
|
|
|
|
|
|
|
Lingua di pubblicazione |
|
|
|
|
|
|
Formato |
Materiale a stampa |
|
|
|
|
|
Livello bibliografico |
Monografia |
|
|
|
|
|
Note generali |
|
Bibliographic Level Mode of Issuance: Monograph |
|
|
|
|
|
|
Nota di bibliografia |
|
Includes bibliographical references (pages [413]-417) and index. |
|
|
|
|
|
|
Sommario/riassunto |
|
The technology of mechanized program verification can play a supporting role in many kinds of research projects in computer science, and related tools for formal proof-checking are seeing increasing adoption in mathematics and engineering. This book provides an introduction to the Coq software for writing and checking mathematical proofs. It takes a practical engineering focus throughout, emphasizing techniques that will help users to build, understand, and maintain large Coq developments and minimize the cost of code change over time. Two topics, rarely discussed elsewhere, are covered in detail: effective dependently typed programming (making productive use of a feature at the heart of the Coq system) and construction of domain-specific proof tactics. Almost every subject covered is also relevant to interactive computer theorem proving in general, not just program verification, demonstrated through examples of verified programs applied in many different sorts of formalizations. The book develops a unique automated proof style and applies it throughout; even experienced Coq users may benefit from reading about basic Coq concepts from this novel perspective. The book also offers a library of tactics, or programs that find proofs, designed for use with examples in the book. Readers |
|
|
|
|
|
|
|
|
|
|
|
|
|
will acquire the necessary skills to reimplement these tactics in other settings by the end of the book. All of the code appearing in the book is freely available online. |
|
|
|
|
|
|
2. |
Record Nr. |
UNINA9910299535603321 |
|
|
Autore |
Everett Helen |
|
|
Titolo |
Faith Schools, Tolerance and Diversity : Exploring the Influence of Education on Students' Attitudes of Tolerance / / by Helen Everett ; edited by Jan Germen Janmaat, Edward Vickers, Henry Everett |
|
|
|
|
|
|
|
Pubbl/distr/stampa |
|
|
Cham : , : Springer International Publishing : , : Imprint : Palgrave Macmillan, , 2018 |
|
|
|
|
|
|
|
|
|
ISBN |
|
|
|
|
|
|
|
|
Edizione |
[1st ed. 2018.] |
|
|
|
|
|
Descrizione fisica |
|
1 online resource (406 pages) : illustrations |
|
|
|
|
|
|
Disciplina |
|
|
|
|
|
|
Soggetti |
|
Religion and sociology |
Educational sociology |
Culture |
Sociology of Religion |
Sociology of Education |
Sociology of Culture |
|
|
|
|
|
|
|
|
Lingua di pubblicazione |
|
|
|
|
|
|
Formato |
Materiale a stampa |
|
|
|
|
|
Livello bibliografico |
Monografia |
|
|
|
|
|
Nota di contenuto |
|
Chapter 1. Introduction -- Chapter 2. Understanding Tolerance -- Chapter 3. The School -- Chapter 4. The Students' Religious Identity -- Chapter 5. The Students' Experience of School -- Chapter 6. Is There Any Difference in Tolerance? -- Chapter 7. Discussion. |
|
|
|
|
|
|
|
|
Sommario/riassunto |
|
This book examines the effects of faith schools on social cohesion and inter-ethnic relations. Faith schools constitute approximately one third of all state-maintained schools and two fifths of the independent schools in England. Nevertheless, they have historically been, and remain, controversial. In the current social climate, questions have been raised about the ability of faith schools to promote Community |
|
|
|
|
|
|
|
|
|
|
Cohesion and, included within that, their ability to promote tolerance. This book explores one aspect of the debate by examining the effect that faith schools have on their students’ attitudes of tolerance. As well as asking what differences exist between students in faith and non-faith schools, it also looks at which aspects of the schools might be affecting the students and their attitudes towards different minorities. The book is a must-read for students and researchers in the fields of education and religious studies, as well as anyone with an interest in the place of faith schools in a modern multicultural society. Helen Everett was, at the time of her death, a Research Manager at the National Foundation for Educational Research. She had taught Science in a variety of English schools before doing her PhD at the UCL Institute of Education, UK, funded by an ESRC award. Jan Germen Janmaat is Reader in Comparative Social Science at UCL Institute of Education, UK. His research focuses on the socio-cultural outcomes of education. He is co-editor of The Dynamics and Social Outcomes of Education Systems. Edward Vickers is Professor of Comparative Education at Kyushu University, Japan. A specialist in the history and politics of education in contemporary East Asia, he is co-author (with Zeng Xiaodong) of Education and Society in Post-Mao China. Henry Everett is the Vicar of St Mary Magdalene and St Peter, Paddington, and is co-author(with Paul Bradshaw and Colin Buchanan) of Coronations Past, Present and Future. He is currently writing on Christian and Muslim shrines. He was married to Helen for 26 years. |
|
|
|
|
|
| |