Re: [Hol-info] [isabelle] definability of new types (HOL), overloaded constant definitions for axiomatic type classes (Isabelle) - Re: Who is ProofPower "by" (and STT)?

general, (B) does not imply (A), and I don't know of interesting sufficient conditions for when it does. Best, Andrei From: Rob Arthan Sent: 23 October 2016 12:23 To: Ondřej Kunčar Cc: Ken Kubota; Prof. Andrew M. Pitts; Prof. Thomas F. Melham; cl-isabelle-us...@lists.cam.ac.uk

[Hol-info] conservativity of HOL constant and type definitions

Since the conservativity topic has been touched upon, I would like to summarize the situation in HOL as I understand it now, after our discussion. (Myself, I am mainly interested in Isabelle/HOL, but this is an important related problem.) Please, correct me if and where I am wrong. (1) The const

Re: [Hol-info] [isabelle] definability of new types (HOL), overloaded constant definitions for axiomatic type classes (Isabelle) - Re: Who is ProofPower "by" (and STT)?

urnal version (and point you to it when it's available). Best, Andrei From: Rob Arthan Sent: 23 October 2016 22:56 To: Andrei Popescu Cc: Ondřej Kunčar; Prof. Andrew M. Pitts; Prof. Thomas F. Melham; cl-isabelle-us...@lists.cam.ac.uk; Roger Bishop Jones;

Re: [Hol-info] conservativity of HOL constant and type definitions

er 2016 21:37 To: Ondřej Kunčar Cc: Andrei Popescu; Prof. Andrew M. Pitts; Prof. Thomas F. Melham; cl-isabelle-us...@lists.cam.ac.uk; Roger Bishop Jones; Prof. Peter B. Andrews; HOL-info list Subject: Re: conservativity of HOL constant and type definitions Ondrej, > On 24 Oct 2016, at 20:32,

Re: [Hol-info] conservativity of HOL constant and type definitions

h equality, Infinity and Choice. Your result is more general. Andrei From: Ramana Kumar Sent: 25 October 2016 08:24 To: Andrei Popescu Cc: Rob Arthan; Ondřej Kunčar; Prof. Andrew M. Pitts; Prof. Thomas F. Melham; cl-isabelle-us...@lists.cam.ac.uk; Roger Bishop J

Re: [Hol-info] On the use of new_axiom() in formal projects

Hi Chun, That paper by Melham is important pioneering work, but will be of little help to you since it only shows how to construct non-permutative datatypes, like lists and ordered trees. The following paper http://andreipopescu.uk/pdf/LICS2012.pdf shows how to construct in HOL (inductive o

Re: [Hol-info] On the use of new_axiom() in formal projects

all. P. S. I?ll still investigate your sample code and the paper I got from Andrei Popescu yesterday, and try to extend my datatype with countably infinite sums (num -> CCS) , but this work will be irrelevant with the proof of the ?last theorem? in my project. Regards, Chun Tian [1] No

Re: [Hol-info] On the use of new_axiom() in formal projects

ious detour from your specific process algebra research. Best regards, Andrei > Il giorno 21 lug 2017, alle ore 23:58, Andrei Popescu > ha scritto: > > Hi Chun, > > That paper by Melham is important pioneering work, but will be of little help > to you since it only shows ho

Re: [Hol-info] On the use of new_axiom() in formal projects

>> Obviously, I am one of the people who find such efforts trustworthy. I meant to write worthwhile -- although they are clearly also trustworthy. :-) Best, Andrei From: Andrei Popescu Sent: 24 July 2017 13:07 To: Chun Tian (binghe) Cc: ho

[Hol-info] POPL tutorial on Isabelle/HOL's codatatypes and corecursion

Dear HOL and Isabelle users, If you are in LA for CPP, POPL etc., please consider attending a Monday (Jan. 8) morning POPL tutorial on recent advances with Isabelle/HOL’s codatatype and corecursion infrastructure. https://popl18.sigplan.org/track/POPL-2018-TutorialFest http://andreipopescu.uk/

[Hol-info] Certified Programs and Proofs (CPP) 2021: First Call for Papers

lso be available via SIGPLAN OpenTOC (http://www.sigplan.org/OpenTOC/#cpp). For ACM’s take on this, see their Copyright Policy ( http://www.acm.org/publications/policies/copyright-policy) and Author Rights (http://authors.acm.org/main.html). PROGRAM COMMITTEE Cătălin Hriţcu, Inria Paris, France (co-ch

[Hol-info] More on "References about mistakes and gaps in papers"

Dear all, This message's subject refers to an old thread on the Isabelle mailing list, from July 2018. This time, I and my coauthor are the protagonists of some "mistakes and gaps"... In impressive recent work, https://arxiv.org/abs/2002.10212 Johannes Åman Pohjola and Arve Gengelbach have form

[Hol-info] Certified Programs and Proofs (CPP) 2021: Final Call for Papers

tp://www.sigplan.org/OpenTOC/#cpp). For ACM's take on this, see their Copyright Policy (http://www.acm.org/publications/policies/copyright-policy) and Author Rights (http://authors.acm.org/main.html). PROGRAM COMMITTEE Cătălin Hriţcu, MPI-SP, Germany (co-chair) Andrei Popescu, University o

[Hol-info] CPP 2021 abstract deadline due soon (in ~23 hours)

Dear potential CPP authors, Please note that, if you intend to submit a paper to CPP 2021, you would need to register it with an abstract very soon, namely by 16 September 2020 at 23:59 AoE (UTC-12h) The submission can be uploaded by 22 September 2020 at 23:59 AoE (UTC-12h). Finally, one piece

[Hol-info] CPP 2021 abstract deadline due very soon

(Apologies for the potential duplication: a previous identical message sent to the list a few hours ago does not seem to have been posted.) Dear potential CPP authors, Please note that, if you intend to submit a paper to CPP 2021, you would need to register it with an abstract very soon, namely b

[Hol-info] two proof-assistant friendly posts of Lecturer in Cybersecurity at University of Sheffield: deadline 3rd December 2020

Greetings, University of Sheffield has opened two posts of Lecturer in Cybersecurity. Details can be found here: https://www.jobs.ac.uk/job/CCG201/lecturer-in-cybersecurity-two-posts Please note that "formalisation and proof of system security properties" is listed first under "suitable areas".

[Hol-info] fully funded PhD position at University of Sheffield on the formal verification of industrial robots

Dear HOL4 users, We have a PhD position at University of Sheffield that can lead to high-impact work using a proof assistant. The PhD project is titled "Formal Specification and Verification of the Safe Interaction between Humans and Industrial Robots" and will be supervised by myself (more about

[Hol-info] fully funded PhD position on verification of industrial robots at University of Sheffield -- application deadline coming soon (Jan. 13)

Greetings, This fast approaching deadline could be of interest to UK or EU residents currently looking for a PhD position and willing to start in mid February. It is an opportunity to do high impact verification research in an excellent academic environment. Background in robotics is not required.

[Hol-info] 21st Midlands Graduate School in the Foundations of Computing Science: Call for Participation

, Birmingham Type Theory Thorsten Altenkirch, Nottingham Proof Theory Anupam Das, Birmingham Advanced courses: Homotopy Type Theory Nicolai Kraus, Nottingham Inductive and Coinductive Reasoning with Isabelle/HOL Andrei Popescu, Sheffield Effects and Call-by-Push-Value Paul Levy, Birmingham

[Hol-info] Lecturer in Verification position at University of Sheffield: deadline 29 March 2021

Greetings, The Department of Computer Science at University of Sheffield has an open position of Lecturer in Verification. Details can be found here: https://www.jobs.ac.uk/job/CEF438/lecturer-in-verification Applicants doing research with and on proof assistants are most welcome. Female applica

[Hol-info] 21st Midlands Graduate School in the Foundations of Computing Science: Final Call for Participation

, Birmingham Type Theory Thorsten Altenkirch, Nottingham Proof Theory Anupam Das, Birmingham Advanced courses: Homotopy Type Theory Nicolai Kraus, Nottingham Inductive and Coinductive Reasoning with Isabelle/HOL Andrei Popescu, Sheffield Effects and Call-by-Push-Value Paul Levy

[Hol-info] Position of Lecturer or Senior Lecturer in Cybersecurity at University of Sheffield

Greetings, The Department of Computer Science at University of Sheffield has an open position of Lecturer or Senior Lecturer in Cybersecurity. Details can be found here: https://www.jobs.ac.uk/job/CFN168/lecturer-senior-lecturer-in-cybersecurity Note that "formalisation and proof of system secur

[Hol-info] PhD position on the formalization of logical calculi in Saarbrücken

A PhD position is open at the MPI for Informatics in Saarbrücken, supervised by Christoph Weidenbach, Jasmin Blanchette and Sophie Tourret. The project is about using Isabelle/HOL to formalize logical calculi. See https://www.cs.vu.nl/~jbe248/sb_job.html for more information. ___

[Hol-info] Certified Programs and Proofs (CPP) 2022: Call for Papers

he official CPP 2022 proceedings will also be available via SIGPLAN OpenTOC (http://www.sigplan.org/OpenTOC/#cpp). For ACM’s take on this, see their Copyright Policy (http://www.acm.org/publications/policies/copyright-policy) and Author Rights (http://authors.acm.org/main.html). PROGRAM COMMI

[Hol-info] Call for Papers: Fifth Workshop on Formal Mathematics for Mathematicians (FMM 2021)

= Call for Papers Fifth Workshop on Formal Mathematics for Mathematicians (FMM 2021) 26-31 July 2021 (exact date TBA) Timisoara, Romania (hybrid or fully virtual) https://cicm-conference.org/2021/cicm.php?event=fmm Co-located with 14th Con

[Hol-info] Certified Programs and Proofs (CPP) 2022: Final Call for Papers

he official CPP 2022 proceedings will also be available via SIGPLAN OpenTOC (http://www.sigplan.org/OpenTOC/#cpp). For ACM’s take on this, see their Copyright Policy (http://www.acm.org/publications/policies/copyright-policy) and Author Rights (http://authors.acm.org/main.html). PROGRAM COMMITTEE Andrei

[Hol-info] 30 months postdoctoral research position at University of Sheffield involving proof-assistant-based verification -- application deadline 23 Sept. 2021

Greetings, A postdoctoral research position (Grade 7) is available at the University of Sheffield. The goal is to perform research in one of the following areas: 1. Formal modelling and verification of security properties for digital twins. This involves the design and development of theoretical

[Hol-info] Certified Programs and Proofs (CPP) 2022: Call for Participation

r generous industrial supporters: https://popl22.sigplan.org/home/CPP-2022 ### Contact For any questions please contact the chairs: Andrei Popescu (PC co-chair) Steve Zdancewic (PC co-chair) Lennart Beringer (conference co-chair) Robbert Krebbers (conferenc

[Hol-info] IJCAR 2022 - Call for Papers

IJCAR 2022 - Call for Papers https://easychair.org/smart-program/IJCAR2022/. ***Important Dates*** Submission deadline February 11, 2022 Start of authors response period April 16, 2022 End of authors response period April 18, 2022 Authors notification April 25, 2022 Overview

[Hol-info] PhD Position in Number Theory and Formalization

The Department of Mathematics of Vrije Universiteit Amsterdam welcomes applications for a fully-funded, 4-year PhD position in Number Theory and Formalization. The preferred starting date is in the period 1 May - 1 September 2022. The candidate will conduct research on Sander Dahmen's NWO-funded

[Hol-info] 22nd Midlands Graduate School, 10-14 April 2022: Call for Participation

CALL FOR PARTICIPATION 22nd Midlands Graduate School (MGS'22) in the Foundations of Computing Science 10-14 April 2022, Nottingham (UK) https://www.cs.nott.ac.uk/~psznk/events/mgs22.html OVERVIEW MGS is an annual spring school that offers an intensive pro

[Hol-info] Position of Lecturer or Senior Lecturer in Cybersecurity at University of Sheffield

Greetings, The Department of Computer Science at University of Sheffield has an open position of Lecturer or Senior Lecturer in Cybersecurity. Details can be found here: https://www.jobs.ac.uk/job/COY785/lecturer-senior-lecturer-in-cybersecurity Note that "formalisation and proof of system secur

[Hol-info] BCS-FACS evening seminar, 24 June 2022: Alan Turing at 110 - and at Oxford!

*Hybrid event: Alan Turing at 110 - and at Oxford!* This hybrid talk celebrates the 110th anniversary of Alan Turing and also explores recent research on his connections with Oxford. Further information and free registration (online and at the BCS London office): https://www.bcs.org/events-calendar

[Hol-info] Sam Staton giving this year's LMS/BCS-FACS Evening Seminar (online) -- registration open until this Wednesday at 5PM, UTC

EVENT: Annual LMS/BCS-FACS Evening Seminar SPEAKER: Sam Staton, University of Oxford TITLE: Programming-based foundations for statistics DATE: Thursday, 17 November 2022, Starting time: 18:00 UTC VENUE: Online via Zoom EVENT PAGE: https://www.lms.ac.uk/events/lectures/lms-bcs-facs-evening-seminar

[Hol-info] PhD or Postdoc Position at LMU Munich about Verified Modal Logics

We are looking for a PhD student (4 years) or postdoctoral researcher (3 years) to work on the Isabelle formalization of modal model theory. The work will take place within the Chair of Theoretical Computer Science at LMU Munich under Jasmin Blanchette's supervision with the participation of two ex

[Hol-info] 3-year Research Associate or Research Assistant position in formal verification, using a proof assistant (preferably Isabelle), at the University of Sheffield

eroot=%2fSAP%2fPUBLIC%2fBC%2fUR%2fuos# Best wishes, Andrei Popescu https://www.andreipopescu.uk/ ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] LMS/BCS-FACS online talk by Lawrence Paulson, 15 January 2024

Dear all, Next week there will be an online talk (via zoom) by Lawrence Paulson on a topic that is likely to be of interest to quite a few people on these lists. Please note the information about registration below. Best wishes, Andrei Information: https://www.bcs.org/events-calendar/2024/janua

Re: [Hol-info] LMS/BCS-FACS online talk by Lawrence Paulson, 15 January 2024

On Mon, Jan 8, 2024 at 11:00 AM Andrei Popescu wrote: > > Dear all, > > Next week there will be an online talk (via zoom) by Lawrence Paulson > on a topic that is likely to be of interest to quite a few people on > these lists. Please note the information about registration belo

[Hol-info] LMS/BCS-FACS Online Seminar, Annabelle McIver, 15 January 2025

*LMS/BCS-FACS Seminar 2025* *Wednesday 15 January 2025, from 19:00 (GMT)Online via Zoom* *https://www.lms.ac.uk/events/lms-bcs-facs-seminar-2025 * In association with the British Computer Society Formal Aspects of Computing Science (BCS-

[Hol-info] Midlands Graduate School 2025 final call -- registration closes on 24 March

Dear Colleagues, There are still slots available at the Midlands Graduate School in the Foundations of Computing Science -- offering eight fantastic courses on category theory, type theory, coalgebra, semantics and more. Registration closes on Monday 24th March, at 1PM GMT. Best wishes, Andrei