6th Indian School on Logic and its Applications
PSG College of Technology, Coimbatore. March 21–26, 2016.
PSG College of Technology, Coimbatore. March 21–26, 2016.
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.
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
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.
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.
Lecture 2 (T S Ramanathan): DeMillo & Lipton, Introduction to bounded arithmetic
Lecture 3 (T S Ramanathan): Natural proofs and independence
Lecture 4 (R Ramanujam): Efficient interpolation and unprovability
Lecture 5 (R Ramanujam): Consequences of unprovability in bounded arithmetic
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.
|9.00 – 10.00||Registration
|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
Registration for ISLA 2016 is closed.
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.
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.
Vijay Elanza, walkable from PSG tech. Ph: 0422 400 4000.
GRT Vibe, walkable from PSG Tech. Ph: 1800 425 55 00.
The Orbis, 2 km from PSG Tech. Ph: 0 422 439 9988.
Zone By The Park, 3 km from PSG Tech. Ph: 0 422 400 5000.
The Residency, 3 km from PSG Tech. Ph: 0422 224 1414.
Vivanta By Taj, 5 km from PSG Tech. Ph: 0422 668 1000.