2024
The Curry-Howard correspondence journey
Proof Society 2024 6th International School and Workshop on Proof Theory, 9-13 September 2024 Birmingham, UK.
Proofs-as-programs: from logic to AI
SMAK 2024 - Serbian Mathematical Congress, 19-22 June 2024, Belgrade, Serbia
Curry-Howard correspondence: new challenges
Correct orchestration of Federated Learning: formalisation and verification
Dagstuhl Seminar, Jan 28 – Feb 02, 2024
Next Generation Protocols for Heterogeneous Systems
2023
Introduction to Barendregt's Lambda Cube
OPLSS 2023 - 21st Oregon Programming Language Summer School, Eugene, USA, invited lectures
CM:FP 2023, Niš, Srbija, invited talk
SCAN 2023, Moscow, Russia, invited talk
LADIS 2.0
Microsoft, Belgrade
2022
Kripke-style semantics in typed lambda calculus, combinatory logic and more
Seminars "Proof Theory" and "Logic Online Seminar" Steklov Mathematical Institute, December 12, 2022, Moscow
Rewriting and Termination in Lambda Calculus
OPLSS 2022 - 20th Oregon Programming Language Summer School, June 20-July 2, 2022, Eugene, USA
Types in Logic, Topology and Structure (invited talk)
Logic and Structure, UNILOG 2022 - 7th World Congress and School on Universal Logic, 1-11 April 2022, Orthodox Academy, Crete
2021
Type Systems for Trustworthiness –- from Mathematics to Large-Scale Systems (keynote)
ECBS 2021 7th Conference on the Engineering of Computer Based Systems, 26-27 May 2021, Novi Sad, Serbia
video
2020
Formal Methods in AI
Privacy-preserving contact tracing (Silvia Ghilezan, Tamara Stefanović)
Webinar Mathematics for Human Flourishing in the Time of COVID-19 and post COVID-19, Ni\v{s}, 21 October 2020
Slides are available on the Webinar web page.
Kripke-style semantics for Full Simply Typed Lambda Calculus (talk given by Simona Kašterović)
LAP 2020 - Logic and Applications, September 21-25, 2020, Dubrovnik, Croatia.
[ slides ]
An Overview of Mathematical Models for Data Privacy talk given by Tamara Stefanović)
LAP 2020 - Logic and Applications, September 21-25, 2020, Dubrovnik, Croatia.
[ slides ]
2019
Towards probabilistic reasoning about typed lambda terms
Logic, Computation and Type Theory Workshop, 16 December 2019, INRIA Sophia Antipolis,
Towards verification of DNNs
Trustworthy Software Workshop, ECNU@UNS - East China Normal University and University of Novi Sad, 3-4 December 2019, Novi Sad.
ECBS 2019 6th European Conference on the Engineering of Computer Based Systems, 2-3 September 2019, Bucharest, Romania.
Towards Completeness of Full Simply Typed Lambda Calculus (Silvia Ghilezan, Simona Kašterović)
TYPES 2020 - 26th International Conference on Types for Proofs and Programs, 2-5 March 2020, Turin, Italy
open access
Denotational and Operational Preciseness of Subtyping
invited talk, Annual meeting of IFIP Working Group 1.6: Rewriting, June 26, 2019, Dortmund, Germany
Logical methods for access control and privacy
UNS @ NTUA: History, Logic, and Algebra day event, Formal Methods Research Group, May 31, 2019, National Technical University of Athens, Greece.
Types in logic, computation and concurrency - an overview
Colloquium Computer Science, May 22, 2019, University of Groningen, The Netherlands.
2018
Doctoral School towards Knowledge Based Society
Invited talk, Serbia for Excell Workshop, Horizon 2020 - Twinning - 2015, June 25-29, 2018, University of Novi Sad, Serbia.
[ video ]
Type-theoretic methods for privacy
Programming Language Seminar, June 11, 2018, University of Oregon, USA.
Precise subtyping for concurrency
Programming Language Club, April 24, 2018, University of Pennsylvania, USA.
Probabilistic reasoning about typed lambda terms
Mathematics - Logic and Computation Seminar, April 23, 2018, University of Pennsylvania, USA.
Types in logic, computation and concurrency - an overview
RIM, University of Kyoto, February 1, 2018, Kyoto, Japan.
Preciseness of Subtyping: from extensional to intensional aspects
NII Shonan meeting 115: Intensional and Extensional Aspects of Computation, January 22-25, 2018, Shonan, Japan.
Probabilistic reasoning about simply typed lambda terms (talk given by Nenad Savic)
LFCS 2018 - Logical Foundations of Computer Science, January 2018, Florida, USA.
2017
Characterization of strong normalizability for a sequent lambda calculus with co-control
PPDP 2017 - 19th International Symposium on Principles and Practice of Declarative Programming, 9-12 October 2017, Namur, Belgium.
Towards Probabilistic reasoning about simply typed lambda terms (talk given by Simona Kasterovic))
VLP 2017 - Probabilistic Logic and Applications, November 8, 2017, Belgrade, Serbia.
Matematički metodi i zaštita privatnosti (Mathematical methods and privacy protection) (invited speaker)
Privatnost u digitalnom dobu: iluzija ili nacionalni izazov 5 October 2017, Belgrade, Serbia.
[ abstract ]
Sound and complete subtyping on intersection and union types
LAP 2017 - Logic and Applications, September 18-22, 2017, Dubrovnik, Croatia.
[ slides ] [ abstract ]
Probabilistic reasoning with lambda terms (talk given by Simona Kasterovic))
LAP 2017 - Logic and Applications, September 18-22, 2017, Dubrovnik, Croatia.
[ slides ]
An Approach to Formally Verified Python Software Transactional Memory (talk given by Branislav Kordic))
ECBS 2017 - 5th European Conference on the Engineering of Computer Based Systems, 31 August - 1 September 2017, Larnaca, Cyprus.
Introduction to Type Theory
EUTypes Summer School, 10-14 July 2017, Ohird, Macedonia.
Characterization of strong normalizability for a sequent lambda calculus with co-control (talk given by José Espirito Santo))
TYPES 2017 - The 23nd Conference on Types for Proofs and Programs, 29 May - 2 June 2017, Budapest, Hungary.
[ abstract ]
Denotational and Operational Preciseness of Subtyping
EUTypes Working Group Meeting, 30-31 January 2017, Ljubljana, Slovenia.
2016
Types for formal systems
Seminar for Constructive Mathematics: Foundations and Practice, 15 December 2016, Nis, Serbia.
Types and Privacy
Invited talk at FMPriv 2016 Formal Methods for Privacy, 7 October 2016, Limassol, Cyprus.
Probabilistic reasoning about simply typed lambda terms (talk given by Nenad Savic))
LAP 2016 - Logic and Applications, September 19-23, 2016, Dubrovnik, Croatia.
[ slides ]
Denotational and Operational preciseness of subtyping for intersection types
International Workshop on Intersection Types, 13-14 June 2016, Paris, France.
Towards probabilistic reasoning about lambda terms with intersection types (talk given by N. Savic))
TYPES 2016 - The 22nd Conference on Types for Proofs and Programs, 23-26 May 2016, Novi Sad, Serbia.
[ slides ]
Tipovi za formalne sisteme (Types for formal systems) (guest speaker)
Seminar Matematickog instituta SANU, 70th Anniversary of the mathematical Institute SASA 13-14 May 2016, Belgrade, Serbia.
Preciseness of Subtyping on Intersection and Union Types (guest speaker)
Seminaire Preuves, programmes et systèmes, Universite Paris Diderot, April 21, 2016, Paris, France.
[ slides ]
2015
Types in access control and privacy
NII Shonan meeting 069: Logic and Verification Methods in Security and Privacy, October 26-29, 2015, Shonan, Japan.
[ slides ]
An optimisation of lambda type assignments via resource control
LAP 2015 - Logic and Applications, September 20-24, 2015, Dubrovnik, Croatia
Normalisation in substructural term calculi
UNILOG 2015 - The 5th World Congress on Universal Logic, June 25-30, 2015, Istanbul, Turkey.
Intersection types fit well with resource control (talk given by P. Lescanne)
TYPES 2015, May 2015, Tallin, Estonia.
Precise subtyping for synchronous multiparty sessions
PLACES 2015 - Programming Language Approaches to Communication- and Concurrency-cEntric Systems, ETAPS 2015, April 18, 2015, London, UK.
2014
Confluence in sequent setting (guest speaker)
UNITO - University of Turin, Dipartimento di Informatica, December 6-14, 2014, Turin, Italy.
Computational approach to logic
VLP 2014 - Probabilistic Logic and Application, October 2-3, 2014, Belgrade, Serbia.
Lambek's computational approach to conjugation
LAP 2014 - Logic and Applications, September 22-26, 2014, Dubrovnik, Croatia.
Preciseness of subtyping on intersection and union types (talk given by M. Dezani)
RTA-TLCA 2014 - 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications, July 14-17, 2014, Vienna, Austria.
Church-Rosser Theorem for sequent lambda calculi
TYPES 2014 Types for Proofs and Programs (within the Special IHP Trimester on Semantics of proofs and certified mathematics), May 12-15 2014, Paris, France.
slides
Grenoble 2014 Cost Action BETTY meeting, (co-located with ETAPS 2014), April 14, 2014, Grenoble, France.
Types in Computation and Communication (guest speaker)
ELTE Eotvos Lorand University, Faculty of Informatics, Feb 17- March 02, 2014, Budapest, Hungary.
[ slides ]
2013
Madrid 2013 Cost Action Richmodels Final meeting, Madrid, 17-18/10/2013
LAP 2013 - Logic and Applications, Dubrovnik, Croatia, 16-21/09/2013 - Reducibility method: an overview 
Reducibility method and logical relations in intuitionistic logic and programming languages (invited speaker)
CM:FP 2013 - Constructive Mathematics: Foundation and Practice, June 24-28, 2013, Nis, Serbia.
Reducibility method and resource control
UNILOG 2013 - The 4th World Congress on Universal Logic, 29/03-04/04/2013, Rio de Janeiro, Brasil,
Roles of Types in Logic, Computation and Security - an Overview (guest speaker)
EPFL - Ecole Polytechnique Federale de Lausanne, Switzerland, LARA - Lab for Automated Reasoning and Analysis, Seminar 27/02-07/03/2013
Rome 2013 Cost Action Richmodels meeting, (co-located with PoPL 2013), Rome, Italy, 20-21/01/2013
2012
Haifa 2012 Cost Action Richmodels meeting, (co-located with HVC 2012) Haifa, Israel, 04/11/2012 - Privacy for Linked Data
SD 2012 - Sustavi dokazivanja, (co-located with LICS 2012) Dubrovnik, Croatia, 29/06/2012 - Računske interpretacije intuicionističke i klasične logike
ITRS 2012 - Sustavi dokazivanja, (co-located with LICS 2012) Dubrovnik, Croatia, 29/06/2012 - Intersection types for explicit substitution with resource control (talk given by J. Ivetic)
Računske interpretacije intuicionističke i klasične logike (guest speaker)
MISANU - Mathematical Institute SASA, Seminar for General Proof Theory, 14/05/2012 abstract
2011
Turin 2011 Cost Action Richmodels meeting, (co-located with FoVeOOS 2011 and FMCO 2011) - Resource control calculi
ICTAC 2011 - The 8th International Colloquium on Theoretical Aspects of Computing Johannesburg, Mabalingwe, South Africa, 31 August - 2 September 2011.
2010
LAC 2010, Paris, France, 16-17/11/2010 - Resource control in sequent lambda calculus
TYPES 2010, Warsaw, Poland, 13-16/10/2010 - Resource control in sequent lambda calculus
Computational interpretations of logic (invited speaker)
HOR 2010 - Higher Order Rewritting (co-located with FLoC 2010), July 14, 2010, Edinburgh, UK.
2009
Tbilisi 2009 - Symposium on Language, Logic and Computation Bakuriani, Georgia, 21-25/09/2009 - Intuitionistic sequent-style calculus with explicit structural rules
2008
PoPL 2008 The 35th Annual ACM SIGPLAN - SIGACT Symposium on Principles of Programming LanguagesSan Francisco, USA, 10-12/01/2008 - An approach to call-by-name delimited continuations
Guest speaker, earlier talks
University of Minho, Portugal (2010), Universite Paris 7, France (2010), University of Florence, Italy (2008), École Normale Superieure de Lyon, France (2007, 2002), University of Turin, Italy (2008, 2002, 2000, 1992, 1991), University of Athens, Greece (2003), Jozsef Atilla University, Szeged, Hungary (1997), University of Nijmegen, The Netherlands (2001, 1991), Universita di Sapienza, Rome, Italy (1992), McGill University, Montreal, Canada (1993), Université de Québéc à Montréal, Canada (1993), University of Utrecht, The Netherlands (1990).
Earlier talks at conferences
TYPES 2007 (Cividale del Friuli, Udine, Italy), WST 2007 (Paris, France), TGC 2006 (Lucca, Italy), LPAR 2005 (Montego Bay, Jamaica), ITRS 2004 (Turcu, Finland), PPDP 2004 (Verona, Italy), TYPES 2003, TYPES 2002, ITRS'02, ICTCS'01 (Turin, Italy), PLS 2001 (Crete, Greece), WST'01 (Utrecht, The Netherlands), ITRS'00 (Geneva, Switzerland), PLS 1997 (Nicosia, Cyprus), BLM 1997 (Barcelona, Spain), LFCS'94 (St.Petersburg, Russia), LMPS 1991 (Uppsala Sweden), Logical Biennial Kleene'90 (Chaika, Bulgaria), Logic Colloquium 1989 (Berlin, Germany).