ALI, the Association for Logic in India, announces the sixth edition of its biennial Indian School on Logic and its Applications (ISLA), to be held at PSG College of Technology, Coimbatore from March 21, 2016 – March 26, 2016. The school is organized by the Department of Applied Mathematics and Computational Sciences, PSG College of Technology.

The Indian School on Logic and Applications is a biennial event. The previous editions of the school were held in IIT Bombay, IIT Kanpur, University of Hyderabad, Manipal University, and Tezpur University. The objective is to present before graduate students and researchers of the country, some basics as well as active research areas in logic. The School typically attracts students and teachers from mathematics, philosophy and computer science departments. The School is complemented by a biennial conference. The sixth conference was held in IIT Bombay, in January 2015. Visit the ALI page for more information about ALI and links to past events.

The theme of this year's school is Logic in Computer Science, and we have some of the best researchers from India lecturing on both basic and advanced topics.

Programme Committee

Organizing Committee

  • Types and Programming Languages
    Sanjiva Prasad (IIT Delhi)

    This course will introduce the connection between logic and programming, and cover briefly the following topics:

    • The untyped lambda calculus
      Minimal intutionistic logic
      Natural Deduction (Sequent calculus)
      Curry-Howard Correspondence: Propositions as Types

    • The simply typed lambda calculus
      Strong Normalisation

    • Polymorphism and ML
      Type-checking and type inference

    • Dependent Types and Intuitionistic Type Theory
      The ML module system

    • Introduction to Coq

  • Petri Nets and connections to logic
    M Praveen (CMI)

    The relation between logics and finite state automata is an important one in computer science. It allows on the one hand to elegantly specify properties using the declarative syntax of logics and on the other hand enables the design of (satisfiability and model checking) algorithms using the structure of automata. Specifying complex properties needs powerful logics. Infinite state systems are known to be useful for some of the more expressive logics. We study one such class of infinite state systems, namely Petri nets, and their connections to logics. We explore second order and temporal logics on strings and fragments of linear logic.

  • Bounded arithmetic and computational complexity
    R Ramanujam (IMSc) and T S Ramanathan (IMSc)

    How difficult is it to prove the assertion P ≠ NP? A natural riposte is to ask: In which proof system? Could it be that the question is formally independent of Zermelo Fraenkel set theory (with Choice)? Early attempts at the problem tried to show relativized unprovability (Hartmanis & Hopcroft), to bound growth rates of functions (DeMillo & Lipton) or to show nonprovability of some exponential bounds (Sazanov). A big departure came in the 1990s when Razborov showed, under cryptographic assumptions, that P vs. NP is independent of certain theories of `bounded arithmetic'. A significant body of work has developed on bounded arithmetic and researchers like Buss, Cook, Krajicek and Pudlak have extensively studied the implications of provability of complexity theoretic assertions in theories of bounded arithmetic.

    These lectures will aim to introduce this line of work and give a flavour of the techniques and results.

  • Logic, types and programming languages II
    Anil Seth (IIT Kanpur)

    In the lectures by Prof. Sanjiva Prasad one would see correspondence between constructive propositional logic and functional programs. In these lectures, we consider its extensions to classical propositional logic. What type constructor corresponds to negation or what is a programming counterpart of a proof by contradiction? Towards this, we present a "continuation" based interpretation of classical logic. Another instance of Curry-Howard isomorphism is second order propositional logic and system F. System F is concise yet very expressive system. We will introduce system F and show how product, sum, inductive, coinductive and existential types can be defined in this system.

  • Descriptive complexity theory: an introduction
    A V Sreejith (CMI)

    In the machine model, languages are categorized based on the physical resources like time and space, needed to express the language. These resources form the fundamental measures of computational complexity. On the other hand, for mathematicians/logicians, the richness of the logic needed to specify a language is more important. In 1974, Fagin showed that the complexity class NP is expressively equivalent to existential second order logic. In short, he showed that the two models of looking at languages are interrelated. Computational complexity is not a model-dependent measure but is more fundamental. After Fagin, researchers were able to show that many computational complexity classes have equivalent logical characterizations. This study is now called Descriptive complexity. Having a different way to look at these classes help us understand them better. For example, Immerman's proof of the Gödel prize winning Immerman-Szelepscenyi theorem, which states that NL is closed under complementation, comes via the descriptive complexity of NL (and non deterministic space classes in general). In this series of lectures, we will look at this fascinating area.

21/03 22/03 23/03 24/03 25/03 26/03
9.00 – 10.00 Registration
Sreejith Ramanujam Ramanathan Anil Anil
10.00 – 10.30 Coffee Break
10.30 – 11.30 Praveen Praveen Sanjiva Sanjiva Sanjiva Anil
11.30 – 12.30 Sreejith Sreejith Ramanathan Ramanujam Ramanujam
12.30 – 14.00 Lunch
14.00 – 15.00 Praveen Praveen Praveen Anil Anil
15.00 – 15.30 Coffee Break
15.30 – 16.30 Sreejith Sreejith Sanjiva Student
16.30 – 17.30 Tutorial Tutorial Tutorial Student
There is an evening of classical music on March 23, 2016, after the academic programme. The excursion on March 25, 2016 is to the Isha Yoga Centre, starting at 16.30.

Registration for ISLA 2016 is closed.

How to reach PSG College of Technology

PSG College of Technology is located in an area called Peelamedu. It is situated at the heart of the city of Coimbatore on the Avinashi Road. There is a foot over-bridge across the road connecting the Academic campus of PSG Tech. and the Residential campus (Guest Houses, Students' Hostels, and Staff Quarters).

It is 5km from the Coimbatore airport and 6km from the Coimbatore Junction railway station. If you are coming from the railway station by auto/taxi, just ask for PSG Tech. If you come by bus, then take a bus for Peelamedu. The bus stops beside PSG College of Technology. You could come inside the college by walk and use the foot over-bridge to reach guest house/hostels.

If you are coming by air, you could use the prepaid taxi services available at the airport. Book a taxi for PSG Tech guest house/ hostel.

Accommodation arrangements

PSG Tech offers a limited number of shared hostel rooms (at Rs. 150 per night) and guest house rooms (at Rs. 300 per night). For those participants who want accommodation outside, there are nice hotels near PSG College of Technology.