[FM-India] ISLA 2022 (Part II) Call for Participation (July 6-8, 20-21, 2022)

[Amaldev Manuel]

Please forward the call for participation below to anyone who might be
interested.

9th Indian School on Logic and its Applications (ISLA 2022)

 (Part-II) (Online)
(July 6-8 & July 20-21, 2022)

In the second volume of ISLA 2022, the following short courses are going to
be offered. All the courses are going to be held online.

   1. Descriptive Complexity Theory

Nikhil Balaji, IIT Delhi (https://sites.google.com/view/nikhilbalaji/home)

Forenoons (10-12 AM), July 6-8

The objective of the course is to understand what functions can one compute
when one  is allowed to use only a constant amount of memory. In a first
course on automata theory one learns that finite automata precisely capture
such algorithms. We will try to capture a relaxed notion of space used by
an algorithm via a model that is a natural generalization of finite
automata, and show an example of some surprising algorithms one can design
in such a model.


   1. Proofs, Programs & Types

Piyush P Kurur, IIT Palakkad (https://piyush-kurur.github.io/)

Afternoons (2:30-4:30 PM), July 6-8

This is a set of 3 lectures of roughly 2 hrs each where I introduce the
participants to writing formal proofs in the proof assistant Coq. Coq
belongs to the family of proof assistants that make use of the
"propositions as types" principle where the type checking of terms in a
(functional) programming language with sufficiently rich type system
(dependently typed languages) can double up as proof checking for
mathematical statements. This has consequences to both the world of
programming and proving.



   1. In Coq we have a programming language where not only can we write
   interesting programs but also prove their correctness. The programs thus
   written are called certified programs and hence come with formal (i.e.
   machine checked) certificates of correctness.

   2. The Coq proof system and its related IDE gives the mathematician an
   interactive environment to prove complicated proofs with high assurance in
   correctness. Domain specific tactics can be designed to automate some of
   the routine steps in the proofs.

The lecture is mainly focused on the former, i.e. writing certified proofs
however, techniques learned here can also help with the latter.

   1. Description Logics

Raghava Mutharaju, IIIT Delhi (http://raghavam.github.io)

Forenoons & Afternoons (10-11 AM, 3-4 PM), July 20-21

Description Logics (DLs) are a family of formal languages based on
first-order logic that are used for knowledge representation and reasoning.
They provide the underpinning for the W3C standard named the Web Ontology
Language (OWL). OWL is used to build ontologies that can capture the
knowledge in a domain in the form of concepts and the relationships between
them.

We will have a series of four lectures where I will discuss the following.

   1.

   Introduce Description Logics and the various constructs used to capture
   the knowledge. I will also discuss some of the languages in the DL family.
   The relationship of DLs with first-order logic and OWL will also be
   discussed.
   2.

   Introduce OWL, its constructs and four different profiles (OWL 2 EL, OWL
   2 QL, OWL 2 RL and OWL 2 DL).
   3.

   Use Protégé, an open-source IDE, to build an ontology with the help of
   the participants.


ISLA is a biennial event of the Association of Logic in India (ALI
<https://logicindiaorg.wordpress.com/>) <https://logicindia.org/>. The
details of the last edition of the school can be found here
<https://sites.google.com/iiserb.ac.in/isla-2020-virtual>.



ISLA 2022 (Part II) Webpage : https://devmanuel.github.io/isla.html

Please register here: https://forms.gle/NFVEfxnmayH2Xbh88

Program Committee:

Amaldev Manuel, IIT  Goa (amal at iitgoa.ac.in)

Sankha S Basu, IIIT Delhi (sankha at iiid.ac.in)

-- 
**************************************************************************

This e-mail is for the sole use of the intended recipient(s) and may

contain confidential and privileged information. If you are not the

intended recipient, please contact the sender by reply e-mail and destroy

all copies and the original message. Any unauthorized review, use,

disclosure, dissemination, forwarding, printing or copying of this email


is strictly prohibited and appropriate legal action will be taken. 


************************************************************************************************