Catégories

[\newcommand\yoneda{ {\bf y}} \newcommand\oppositeName{ {\rm op}} \newcommand\opposite[1]{ {#1}^\oppositeName} \newcommand\id[1][{}]{ {\rm id}{#1}} \newcomma...

Sydney Reading Group: Classifying Category

[\newcommand\yoneda{ {\bf y}} \newcommand\oppositeName{ {\rm op}} \newcommand\opposite[1]{ {#1}^\oppositeName} \newcommand\id[1][{}]{ {\rm id}{#1}} \newcomma...

Lecture 1 : Speedup theorem

Outline

Exercises 1 : SPACE and NL

EX 1: Graph representation and why it doesn’t matter

Lecture 2: Logspace

Webpage of the course

Exercises 2 : SPACE and NL (2)

EX 1 : Warm up

Lecture 3:

Immermann-Szelepcsenyi (1987)

Exercises 3: Space hierarchy theorem

EX 1: Space hierarchy theorem

Lecture 4: Alternating Turing Machines

Recap:

Exercises 4: PSPACE-complete problems, Padding

EX 1: Language theory

Lecture 5: P=AL

Last week:

Exercises 5: Prime Numbers, P-complete problems

EX 1: Unary languages

DM: Advanced Complexity

Homework Assignment : Advanced complexity.

Lecture 6: Polynomial-time hierarchy

A visit to the polynomial-time hierarchy

Lecture 7: RP, coRP, ZPP, BPP

RP, coRP, ZPP, BPP

Exercises 10: BPP, AM protocols, AM hierarchy

EX0: BPP-completeness

Lecture 8: BPP, P/Poly

Karp-Lipton

Exercises 11: BPP, ABPP, PP

Proofs to bear in mind

Lecture 9: The PCP theorem

cf. CSE 533: The PCP Theorem and Hardness of approximation (autumn 2005)

Exercises 12: Review

NP, coNP

Computational Geometry Learning: Introduction

Teacher: Marc Glisse

Homology theory

Teacher: Clément Maria

Discrete Morse theory

Teacher: Clément Maria

Persistent Homology

Cech complex

Compatible basis, Stability of persistent homology, and Homology inference

[K_0 = ∅ \overset{σ_1}{\hookrightarrow} K_1 \overset{σ_2}{\hookrightarrow} K_2 \overset{σ_3}{\hookrightarrow} ⋯ \overset{σ_n}{\hookrightarrow} K_n = \lbrace ...

Lecture 1: Reinforcement learning

Stimulus $u_i$ Reward $r_i$ Expected reward: $v_i ≝ w u_i$ Prediction error: $δ_i = r_i - v_i$ Loss: $L_i ≝ δ_i^2$

Lecture 2: Receiver-operating characteristics

Neurons act as if they were performing reinforcement learning.

Lecture 3: Population Coding and Decision-Making

Population Coding: how neural activities relate to an animal’s behavior

Lecture 4: Addiction

Addiction: affects all parts of the brain

Lecture 5: The Binary Neuron model

Teacher: Grégory Dumont

Lecture 6: Biophysics of neurons

Teacher: Grégory Dumont

Cours 1 : Introduction

Livres de référence:

Cours 2: Géométrie projective

Trois réglages clefs dans appareil photo:

Cours 3: Matrice d’une caméra

Projets:

TP1: Canny Edges

Practical session 1: Canny Edges

TP2: Optical flow: zero normalized cross-correlations, Lukas Kanade algorithm

Practical session 2: Optical flow

TP4: Neural Networks

Practical session 4: Neural Networks

TP3: Mean Shift

Practical session 3: Mean Shift

Cours 4: Réseaux de neurones

R-CNN

Optional TP: Calibration

Practical session: Calibration

Final Summary: Dimensionality Reduction and Visualization of Representations

Final Summary for the final presentation

Directed Algebraic Topology and Concurrency: Introduction

Teacher: Emmanuel Haucourt

Pospaces, Local pospaces

Recap: every program in our setting is comprised of sequential processes $(P_1, …, P_n)$ that are turned into a control flow graph $(G_1, …, G_n)$

Metric spaces, Pospaces and Local pospaces

Metric Spaces

Geometric models

Cartesian product

Isothetic regions

Stages

Page du cours

Conférences (Rapports L3) 1er Septembre

Algorithme de placement de processus à l’aide de modèles enrichis

Conférences (Rapports L3) 1er Septembre

Représentation et analyse des phénomènes de coercion en sémantique des cadres

Conférences (Rapports L3) 1er Septembre

Quantum Computing

Conférences (Rapports L3) 6 Septembre

SQL query evaluation with correctness guarantees

Conférences (Rapports L3) 8 Septembre

Implementation of an attack on NTRU assumption

Conférence Varsovie 1 : Game Theory

Oskar Skibski :

Conférences (Rapports L3) 1er Septembre

Assistants de preuves Assia Mahboubi

Conférences (Rapports L3) 1er Septembre

A la recherche du son 3D - François Alouges Question : est-ce qu’on peut imiter l’écoute 3D avec un casque ?

Véronique Cortier : Vote électronique

Véronique Cortier : équipe “méthodes formelles” au LORIA, à Nancy.

Tutorat: Cours 1

Enseignante: Valérie Péris-Delacroix

Lecture 1: Introduction

Teacher: Paul-André Melliès

Lecture 2: Introduction to Domain theory

Teacher: Paul-André Melliès

Lecture 3: Cartesian closed categories

Teacher: Paul-André Melliès

Execises 2: Stable models of $λ$-calculus

Teacher: Paul-André Melliès

Lecture 4: Simply typed λ-calculus as CCC

Teacher: Paul-André Melliès

Lecture 5: Coherence spaces

Teacher: Paul-André Melliès

Lecture 6: Monoidal Categories

Teacher: Paul-André Melliès

Lecture 7: Step functions and exponential modalities

Teacher: Paul-André Melliès

Lecture 8:

Teacher: Paul-André Melliès

Lecture 9: Lazy PCF

Teacher: Thomas Ehrhard

Execises 3: Coherence spaces and lazy integers

Teacher: Thomas Ehrhard

Lecture 10: Categorical combinators, Categorical Abstract Machines

Teacher: Pierre-Louis Curien

Lecture 11: Categorical model of LL and Eilenberg-Moore category of $!$

Teacher: Thomas Ehrhard

Lecture 12: $PoL$, $PoLR$, $PoC$ categories

Lecture 12

Lecture 13: Scott semantics

Lecture 13

Lecture 14: Sequentiality, Concrete Data Structures

Full Abstraction

Lecture 15: Realisability, $PoLR_!$ not fully abstract

Lecture 15

Lecture 16: Sequential Algorithms

Lecture 16

Lecture 17: Or-tester, Abstract algorithms

Lecture 17

Lecture 18: PCF Böhm trees, Innocent strategies, Hyland-Ong Games

Lecture 18

Lecture 19: Systematic compilation of PCF Böhm Trees

II.

Algèbre 1

1.

TD Algèbre : Anneaux

Énoncé

Lecture 1: Proofs in theories

Teacher: Gilles Dowek

Exercise Sheet 1

Teacher: Gilles Dowek

Lecture 2: Models

Teacher: Gilles Dowek

Lecture 3: Arithmetic

Teacher: Gilles Dowek

Exercises 2: Termination of $β$-reduction and Simple Type Theory

Teacher: Gilles Dowek

Lecture 4: Simple Type Theory

Teacher: Gilles Dowek

Lecture 5: Termination of proof reduction in Deduction modulo theories

Teacher: Gilles Dowek

Exercises 3: Term associated to a proof, Leivant/Krivine/Parigot arithmetic

Teacher: Gilles Dowek

Lecture 6: Dependent type theory

Teacher: Gilles Dowek

Lecture 7 (Master Class): Negative translation

Teacher: Valentin Blot

Lecture 1: Operational semantics and reduction strategies

Teacher: François Pottier

Lecture 2: Verified Interpreters

Teacher: François Pottier

Lecture 3: Closure conversion, Defunctionalization

Teacher: François Pottier

Lecture 4: Continuation Passing Style

Teacher: François Pottier

Lecture 5: Functional programming

Teacher: Didier Remy

Proof of programs with Why3

Teacher: François Bobot

[Why3 Project] Computational Reals

Github Repo Report

[Functional Programming Project] Compiling simply typed λ-calculus to Categories: Automatic Differentiation

Functional programming MPRI project (teachers: Yann Régis-Gianas, François Pottier, Pierre-Évariste Dagand and Didier Rémy), about compiling simply typed...

Lecture 1: Zero-sum perfect information games, Reachability games

Teachers: Wieslaw Zielonka

Lecture 2: Büchi condition

Teachers: Wieslaw Zielonka

Lecture 3: Games on graph

Teachers: Dietmar Berwanger

Lecture 4:

Teachers: Dietmar Berwanger

Lecture 1: J eliminator, Truncation, Extensional type theory

Correspondence between Types and Topological spaces

Lecture 2: Equivalences

Recall that

Lecture 3: Inductive/co-Inductive types

Examples of inductive types:

Lecture 4: Streams

Streams:

Lecture 5: Higher Inductive Types

HIT: Inductive types where equality is also taken into account.

Lecture 6: Encoding of $λ$-calculus, System T & System F

[μC. (C ⟶ C)]

Lecture 7: Category theory in HoTT

We want a notion of category where type is a category, so that there’s a notion of homotopy thanks to model structures.

Lecture 8: Categories in 2-level type theory, Fibrations and co-Fibrations

Category in 2-level type theory

Lecture 8: Cubical type theory

Globular Sets

Lecture 1: Categorical reminders

Teacher: Benjamin Hennion

Lecture 2: Abelian Categories

Teacher: Benjamin Hennion

Lecture 3: Resolutions

Teacher: Benjamin Hennion

Lecture 4: Ext Functors, Sheaves, Double complexes

Teacher: Benjamin Hennion

Lecture 5: Künneth formula, Simplicial objects, Dold-Kan correspondence

Teacher: Benjamin Hennion

Cours 1 : 𝛽-réduction et 𝛼-renommage

$\sim$ 1930 : Alonzo Church.

TD1 : 𝛽-réduction et 𝛼-renommage

Énoncé

TD2 : graphes de réduction

Énoncé

TD3 : stratégies et combinateurs

Énoncé

TD4 : Modèles du 𝜆-calcul

Énoncé

Cours 2 : Modèles du 𝜆-calcul

Modèle du $𝜆$-calcul

Cours 2 : 𝜆-calcul simplement typé

$𝜆$-calcul simplement typé

TD7 : 𝜆C, Non-non traduction, logique intuitionniste

Énoncé

TD8 : Paradoxe de Russel

Énoncé

DM: Quelques modèles de graphes du 𝜆-calcul

DM de $𝜆$-calcul

TD10 : types de données en $𝜆$-calcul

Énoncé

TD9 : Système F

Énoncé

TD11 : $HA_2$ et Ackermann

Énoncé

Cours 4 : Introduction à la réécriture et la décision modulo, par Frédéric Blanqui

Rappels

Cours 1 : Introduction

Introduction

Cours 2 : Automate minimal

Automate minimal

TD 1 : Introduction

Énoncé

TD 2 : Dérivées partielles, Antimirov, Glushkov

Énoncé

TD 3 : Minimisation

Énoncé

Cours 3 : Langages algébriques

Langages algébriques

TD 4 : Langages algébriques

Énoncé

Cours 4 : Langages algébriques, suite

On this page

TD 5 : Lemme d’Ogden

Énoncé

Cours 5 : Automates à pile

Définition

Cours 6 : Partie avant d’un compilateur

Partie avant d’un compilateur

Cours 7 : Analyse syntaxique ascendante

Analyse syntaxique ascendante

Cours 8 : Automates à double sens, Automates séquentiels

Automates à double sens

DM : Automates à pile déterministes

DM : Deterministic Pushdown Automata

TD 6 : Automates à pile

Énoncé

TP : Langages Formels

TP de Langages Formels

TD 8 : Accessibilité dans les grammaires algébriques

Énoncé

TD 9 : Lemme de Dickson, PDA et logique MSO

Énoncé

TD 10 : Reconnaissance par morphisme, machines de Moore et automates de Mealy

Énoncé

TD 11 : Automates pondérés, logique MSO et AFP

Quelques exemples

TD 12 : Fonctions séquentielles, Automates à pile déterministes

EX 1

TD 13 : Langages déterministes, acceptation par pile vide, acceptation généralisée, non-ambiguïté

EX 1

DM : Automates pondérés

DM : Automates pondérés.

TD 14 : Logique temporelle linéaire, Automates d’arbres

EX 3

TD 15 : Automates d’arbres ascendants et descendants

EX 1. Automates d’arbres

Lecture 1: Hilbert Calculus, Natural Deduction, Sequent Calculus

Teacher: Michele Pagani

Exercise Sheet 1:

Teacher: Michele Pagani

Exercise Sheet 3:

Teacher: Delia Kesner

Lecture 2: MLL/MALL/MELL, Lafont menu, Negative encoding

Teacher: Michele Pagani

Lecture 3: Proof nets

Teacher: Michele Pagani

Lecture 4: Cut-elimination for MLL

Teacher: Michele Pagani

Lecture 5: Language-oriented MELL

Teacher: Delia Kesner

Lecture 6: MELL Proof nets

Teacher: Delia Kesner

Lecture 7: Static translation

Teacher: Delia Kesner

Lecture 8: $λlxr$-calculus vs. $λ$-calculus

Teacher: Delia Kesner

Lecture 9: Cost models

Teacher: Beniamino Accatoli

Lecture 10: Abstract Machines

Reminder:

Lecture 11:

Important concepts in rewriting theory: when redexes are created

TD: Abstract Machines

Exercise 1

Lecture 12: Building Intuitionistic and Classical proofs

Teacher: Dave Miller, INRIA

Lecture 13: Abstract Logic Programming

Abstract Logic Programming: Proof theory formulations (corresponds to chapter 5 in Dave Miller’s lecture notes)

Lecture 14: The $\bullet ; \bullet ⊢_o \bullet$ Proof System

[⊢_O = ⊢_I = ⊢_C \qquad hC ⊆ hH \qquad ⊢_O = ⊢_I]

Cours 1 : Introduction

Introduction

Cours 2 : Complétude et Complétude réfutationnelle

Complétude

Cours 3 : Déduction naturelle

Déduction naturelle : Pas utilisée en pratique

Cours 2 : Logique intuitionniste et sémantique de Kripke

Calcul des séquents

TD 1 : Introduction

Énoncé

TD 2 : Formes clausales et résolution

Énoncé

TD 3 : Stratégie de résolution et déduction naturelle

Énoncé

TD 4 : Systèmes de preuve classique et inuitionniste

Énoncé

Logic Project : SAT solver

Naive and DPLL algorithms

TD 5 : Sémantique de Kripke

Énoncé

Cours 5 : Logique du premier ordre

Theories

DM : QBF et la logique intuitionniste

TD 6 : Herbrand, Compacité et Unification

EX 1

TD 7 : Herbrand & Prolog

EX 2

Cours 6 : Programmation logique

Programmation logique

Cours 7 : Théories axiomatiques

Introduction

Cours 8 : Théories indécidables

Théories indécidables

TD 8 : Théories

EX 1

Cours 9 : Deuxième théorème d’incomplétude de Gödel, Jeux d’Ehrenfreucht-Fraïssé

Introduction

TD 9 : Révisions générales

EX 1.

TD 10 : Cohérence, récursivité, complétude, argument diagonal

Théories & Gödel

TD 11 : Exemples, Herbrand

EX 1. Théories cohérentes

TD 12 : Argument diagonal, modèles non standards, classe de Bernays-Schönfinkel

EX 1

TD 13 : Satisfiabilité, Résolution, complétude

Enoncé

Lecture 1: Bayesian perception

Lecturer: Pantelis Leptourgos

Lecture 2: Probabilistic approaches to neural computation: the Bayesian Brain

Lecturer: Lyudmila Kushnir

Problem Set 1: Gaussian Neuronal Noise & Discriminability

Problem 1: Gaussian Neuronal Noise

Lecture 3: Supervized and Unsupervized learning

Lecturer: Mirjana Maras

Lecture 4: Pooled population data

Lecturer: Mirjana Maras

Lecture 5: Reinforcement Learning

Lecturer: Lyudmila Kushnir

Problem Set 3: Reinforcement Learning

Problem 1

Lecture 6: Graphical Models and Inference

Lecturer: Pantelis Leptourgos

Lecture 7: Receptive fields

Lecturer: Sophie Denève

Lab: K-means and expectation maximization algorithms

Lecturer: Lyudmila Kushnir

Lecture 8: Coding and computing with balanced spiking networks

Lecturer: Sophie Denève

Lab: Efficient balanced networks

Lecturer: Lyudmila Kushnir

[Project] Memory Evolutive Neural Systems (MENS)

Final Project: Coherent Patterns of Activity from Chaotic Neural Networks.

Cours 1 : Cardinalité, Lemme d’Erdös, Formule du crible

Prof : Claudine Picaronny picaro@lsv.ens-cachan.fr

TD1 : Dénombrement

Chargé de TDs : Anthony Lick

TD2 : Équipotence, Dénombrabilité

TD 2

Cours 2 : Relations binaires/d’équivalence/d’ordre, Diagramme de Hasse, Treillis

Chapitre 2 : Relations

Cours 3: Structures algébriques, Catégories, Semi-groupes, Monoïdes libres/finis

Chapitre 3 : Structures algébriques

Cours 4 : Groupes, Actions de groupe, Formule de Burnside

Groupes

Cours 5 : Anneaux

Anneaux

TD3 : Relations d’équivalence, Chaînes

TD 3

TD4 : Relations d’ordre

EX 1

TD5 : Équations de mots, Groupe symétrique

EX 1

TD6 : Groupes cycliques, Actions de groupe et théorème de Fermat, Séries Formelles, Nombres de Catalans

1. 1.

DM1 : Théorème de Dilworth, Nombres de Catalan, Partitions entrelacées

Maths Discrètes : DM1

Fiche-Résumé : Cours 1 à 5

Version PDF

Cours 6 : Probabilités

Introduction

TD7 : Probabilités, Loi uniforme, Pile ou face

EX 1

TD8 : Probabilité d’être un multiple de a, Problème du secrétaire

EX 1

TD8 : Chaînes de Markov

EX 1

Cours 7 : Chaînes de Markov

Chaînes de Markov :

TD10 : Constante de Frobenius

EX 1

Cours 8 : Théorèmes limites et convergences de processus

I. Différents types de convergence

DM2 : Problème des anniversaires, Séries génératrices, Arbres aléatoires

Maths Discrètes : DM 2

DM3 : Chaînes de Markov.

Maths Discrètes : DM 3

Cours 9 : Statistiques

Statistiques : Aperçu

Fiche-Résumé 2 : Cours 6 à 8

Version PDF

MathPark : Nombres de Catalan

Introduction

Cours 1 : Introduction

Adjonction: représentations $𝕂$-linéaires sur $M$ / $𝕂[G]$-modules sur $M$

TD1 : Suites exactes

EX 1.2.4

Cours 2 :

Extension/restriction des scalaires

TD2 : Produits tensoriels

EX 1.2.10

DM : permutations conjuguées, $p$-Sylow

DM: Groupes finis.

TD3 : Caractères

EX 3.2.5.

Lecture 1: Neurorobotics

La robotique peut aider les neurosciences :

Lecture 2: Perception en robotique

David Filliat

Tutorial 1: Reinforcement Learning

Lecture 3: Neurorobotic models of spacial cognition

Teacher: Anfelo Arleo

Lecture 4: Neuromimetic Navigation Strategies

Teacher: Benoît Girard

Lecture 5: Bayesian filters

Teacher: Bessière Pierre

Tutorial 2: Navigation Strategies

Tutorial 3: Regression

Lecture 6: Perception et émotion pour l’interaction

Teacher: Philippe Gaussier

Lecture 7: Motor Control

Teacher: Emmanuel Guigon (ISIR, Sorbonne Université)

Lecture 8: Evolutionary Robotics

Teacher: Stéphane Doncieux, Nicolas Bredèche

[Final Project] Inferring Space from Sensorimotor Dependencies

Documentation Slides iPython notebook

Tutorial 4: Intent Recognition

Lab 4: Intent Recognition Younesse Kaddar, Alexandre Olech and Kexin Ren (Lecturer: Mohamed Chetouani)

UE Cognition Conférence: Penser

Introduction : qu’est-ce que c’est que penser ?

Cours 1: Introduction

Neurosciences: introduction

Cours 2: Moelle spinale, Tronc cérébral

Moelle spinale

Cours 3: Coupes coronales sériées

Coupes coronales sériées

Introductive tutorial: Evolution of a population

Introductive tutorial

Problem Set 2: Quantitative models of behavior

Problem Set 2: Quantitative models of behavior.

[Problem Set 2 Quantitative models of behavior] Problem 1: Rescola-Wagner Rule

Problem 1: The Rescola-Wagner Rule

[Problem Set 2 Quantitative models of behavior] Problem 2: Decision strategy for flower sampling by bees

Problem 2: Decision strategy for flower sampling by bees.

[Problem Set 2 Quantitative models of behavior] Problem 3: The drift diffusion model of decision-making

Problem 3: The drift diffusion model of decision-making.

[Problem Set 2 Quantitative models of behavior] Problem 4: Reinforcement learning in a maze

Problem 4: Reinforcement learning in a maze.

Problem Set 3: Spike trains

Problem 1: Poisson spike trains.

[Problem Set 3 Spike trains] Problem 1: Poisson spike trains

Problem 1: Poisson spike trains.

[Problem Set 3 Spike trains] Problem 2: Analysis of spike trains

Problem 2: Analysis of spike train.

[Problem Set 3 Spike trains] Problem 3: Integrate-and-Fire neuron

Problem 3: Integrate-and-Fire neuron.

[Problem Set 3 Spike trains] Problem 4: The Hodgkin-Huxley model

Problem 4: the Hodgkin-Huxley model.

Problem Set 4: Networks

Problem Set 4: Networks.

[Problem Set 4 Networks] Problem 1: Neuron with Autapse

Problem 1: Neuron with Autapse.

[Problem Set 4 Networks] Problem 2: Circuit with mutual inhibition

Problem 2: Circuit with mutual inhibition.

[Problem Set 4 Networks] Problem 3: Hopfield model

Problem 3: Hopfield model.

Lecture 1: Neuromodeling

Manuel Beiran: manuel.beiran-at-ens.fr

Lecture 2: Rescorla-Wagner Rule

Classical conditioning

Lecture 3: Exploration-exploitation dilemma

Computational model of behavior:

Lecture 4: Drift-diffusion models

Reminder: differential equations we’ll encounter

Lecture 5: Integrate-and-fire neurons

A Cell ⟺ An RC circuit

Lecture 6: Hodgkin-Huxley model

Cell membrane = semi-permeable

[Project] Coherent Patterns of Activity from Chaotic Neural Networks

Final Project: Coherent Patterns of Activity from Chaotic Neural Networks.

Algèbre Linéaire : Valeurs propres imaginaires pures

MathJax + Version PDF

Florilège d’exercices : Exercice 1

Version PDF

Florilège d’exercices : Exercice 10

Version PDF

Florilège d’exercices : Exercice 11

Version PDF

Florilège d’exercices : Exercice 12

Version PDF

Florilège d’exercices : Exercice 13

Version PDF

Florilège d’exercices : Exercice 14

Version PDF

Florilège d’exercices : Exercice 15

Version PDF

Florilège d’exercices : Exercice 16

Version PDF

Florilège d’exercices : Exercice 17

Version PDF

Florilège d’exercices : Exercice 18

Version PDF

Florilège d’exercices : Exercice 19

Version PDF

Florilège d’exercices : Exercice 2

Version PDF

Florilège d’exercices : Exercice 20

Version PDF

Florilège d’exercices : Exercice 21

Version PDF

Florilège d’exercices : Exercice 3

Version PDF

Florilège d’exercices : Exercice 4

Version PDF

Florilège d’exercices : Exercice 5

Version PDF

Florilège d’exercices : Exercice 6

Version PDF

Florilège d’exercices : Exercice 7

Version PDF

Florilège d’exercices : Exercice 8

Version PDF

Florilège d’exercices : Exercice 9

Version PDF

Florilège d’exercices : tous les exercices

Version PDF

Probabilités : Loi hypergéométrique

MathJax + Version PDF

Analyse : Fonction de McCarthy

Version PDF

Lemme : fonction uniformément continue qui admet une intégrale

MathJax + Version PDF

Système différentiel : orbites

MathJax + Version PDF

TIPE 2015 : Mouvement Brownien et Détermination du nombre d’Avogadro

Détermination du nombre d’Avogadro

TIPE 2016 Résumé : Théorie des modèles

MathJax + Version PDF

TIPE 2016 Transparents : Théorie des modèles

MathJax + Version PDF

TIPE 2016 : THÉORIE DES MODÈLES, DE L’EXEMPLE AU MODÈLE (Version Exhaustive)

MathJax + Version PDF

Dependent types and HOL

Dependent Types

TD8: Définitions inductives de prédicats

Page du cours

HOL

Symmetry in HOL

TD9: Enigme de MU: Définitions inductives de prédicats et analyse par cas

TD9 : Définitions inductives de prédicats et analyse par cas

Isabelle

Isabelle (named by Lawrence Paulson after the daughter of Gérard Huet, as a tribute): a popular generic theorem prover

TD10: Damier (checker)

NB: Boards are finite. Number of configurations:

[Final Coq Project] Coherence of Heyting’s arithmetic

Coherence of Heyting’s arithmetic in Coq

Cours 1: Algèbre initiale

Algèbre intiale (pour un foncteur)

Cours 2: cohérence de $PA_2$, Girard et Takeuti

Imprédicativité:

Cours 3: Candidats de réductibilité de Tait

Comment pallier le problème de définition circulaire des candidats de réductibilité $Red(∀X. A)$ ?

Cours 4: Normalisation du système F

Expression, dans Peano, du fait que $Red_ρ(A)$ est un candidat de réductibilité:

Cours 5: Sémantique dénotationnelle

Introduction

Cours 6: Domaines de Scott

Dans une Catégorie Cartésienne Close (CCC)

Cours 7: Espace cohérents

Espaces cohérents

Cours 8: La catégories des espaces cohérents est monoïdale close

Catégories $Coh$ et $Stab$

Cours 9: Logique linéaire

Rappel: Le bang $!: Stab ⟶ Coh$ est l’adjoint à gauche du foncteur d’oubli $𝒰: Coh ⟶ Stab$:

Cours 10: Traduction de Girard et Substitution explicite

Traduction de Girard

Cours 11: Réseaux de preuves

Réseaux de preuves pour MLL

Cours 12: Axiomatisation catégorique de la logique linéaire

Rappels

Cours 13: Théorème de Friedman: correction

Nouveau professeur pour cette seconde partie : Michele Pagani

Cours 14: Théorème de Friedman: complétude

Friedman:

Cours 15: PCF

Expressivité

Cours 16: PCF: Logical Relations to show Adequacy

Rappels

Cours 17: Fully abstract models

Th: Let $M$ be a PCF program, then \[⟦M⟧ = n \text{ iff } M ⟶^\ast \underline{n}\]

Cours 18: Catégorie des Espaces Cohérents: Modèle de PCF

cf. Linear Logic, Girard (1987)

Cours 19: Probabilistic Coherence Spaces and the $PCoh$ category

Caractérisation des espaces cohérents

Cours 20: Probabilistic Coherence Spaces and Linear Logic

In Probabilistic Coherence Spaces, $𝒫(𝒜)$ is closed under $\sup$

TD: La catégorie $PCoh$

1. Le produit monoïdal $\otimes$ de $PCoh$

Projet de Programmation : Compilateur C–

Méthode utilisée pour compiler les exceptions

Cours 1 : Introduction aux langages de programmation, Représentation des entiers

TD12 : flux d’information sûrs

TD : flux d’information sûrs

TD2 : Assembleur

TD2 de Programmation 1

TD4 : Pointeurs, Copies profondes

3

TD5 : Modes d’appel, Portée

1. Portée

TD6 : Sémantique

Simon Halfon :

TD7 : Adéquation, Théorèmes du point fixe, DCPO

1.

TD8 : DCPO, Topologie de Scott

EX 1

TD9 : Sémantique

EX 1

Cours 2 : Architecture, Console, Assembleur

TD1 : Entiers, flottants, encodage

TD 1

Mini-Projet

Travail effectué

Cours 3 : Structures de données en C, Types VS Classes de stockage, Arithmétique des pointeurs

Structures de données

Cours 4 : Modes d’appels, Portée lexicale/ Liaison dynamique

Modes d’appels

Cours 5 : Sémantique

Sémantique

TP Programmation

DM : Programmation 1

DM Programmation I

Cours 7 : PCF

Plotkin et le PCF

Programmation 2 : Modules

Etienne Lozes

Lecture 1: Introduction

Teachers: Bruno Barras & Matthieu Sozeau

Lecture 2: Martin-Löf’s Type Theory, System F, Calculus of Constructions

Teachers: Bruno Barras & Matthieu Sozeau

Lecture 3: Inductive Types

Teacher: Bruno Barras

Lecture 4: Models

Teacher: Bruno Barras

Presentation: Introduction

Goals

Serendipity Workshop

Recommandation

Serendipity Workshop

Article: http://www.sciencedirect.com/science/article/pii/S221083271400026X

Article: Generalized Relations in Linguistics and Cognition

Link of slides

Lecture 1 : Capteurs et actionneurs

Planification de mouvement

Lecture 2: Optimisation, Géométrie inverse

Optimisation convexe

Lecture 3: Holonomic Distributions

Differential Geometry

Final Report: Motion of Objects in Contact (Hopcroft & Wilfong)

Rapport: Mouvement d’Objets en Contact

Lecture 1: Supervised Machine Learning

Outline

Lecture 2: Regression

Linear Regression and Logistic regression: particular cases of empirical risk regression

TP1: Linear Regression

Practical session 1: linear regression

Lecture 3: $k$-nearest neighbors

kNN: k-nearest neighbors

Lecture 6: PAC-Learning

Probably Approximately Correct

Lecture 4: Convex analysis/optimization

Convex functions

Exercises: Convex optimization

Practical session 3: linear regression

TP2: $k$-nearest neighbors

Practical session 2: kNN

Lecture 5: Convex analysis/optimization

Convex optimization

Exercises 5: Learning theory and PAC bounds

Practical session 5: Learning theory and PAC bounds

Lecture 7: Maximum likelihood

Maximum likelihood

Exercises 6: Learning theory and PAC bounds

Practical session 5: Learning theory and PAC bounds

TP6b: Régression linéaire & logistique, Analyse discriminante linéaire & quadratique

Practical session 4: Convex optimization

TP4: Convex optimization

Practical session 4: Convex optimization

Lecture 8: Reinforcement learning, Online Learning

Online learning

Lecture 9: Apprentissage non supervisé

Introduction

Practical session 10: LASSO Regression

Lecture 10: Summary

Summary of the class

TD 12: Révisions

Practical session 12: Summary

TP 11: PCA et $K$-Means

Practical session 11: PCA and K-Means

Introduction: Vue d’ensemble

Théorie des modèles : vue d’ensemble

Cours 1: Rappels

Notations et rappels

Extension élémentaire commune, Amalgamation élémentaire, Applications élémentaires partielles

Teacher: Tomas Ibarlucia

Va-et-vient

Teacher: Tomas Ibarlucia

Résultats de préservation

Teacher: Tomas Ibarlucia

Modèle complétude et théories modèle compagnes

Teacher: Tomas Ibarlucia

Elimination des quantificateurs pour ACF, Types

Teacher: Tomas Ibarlucia

Espace des types

Proposition: On se fixe $ℳ, \; A ⊆ M, \; \overline{x}, \; p = p(\overline{x})$ un ensemble de $ℒ_A$-formules. Si $𝒩 \succcurlyeq ℳ$, alors ...

Notes de cours (Ilia Itenberg)

Topologie générale

Cours 1: Version faible de Van Kampen

7. Version faible du théorème de Van Kampen

Cours 2: Revêtements

Ch 4. Revêtements

TD 1: Topologie générale, Espace quotient

Feuille 1

Lecture 1: Introduction

Introduction

Exercises 1 : Recognizable Tree Languages and Finite Tree Automata

EX 1: First constructions

Lecture 2: Languages that aren’t regular tree ones

[L_1 ≝ \lbrace f(g(a, \square, b)^n \circ d, h(\square, c)^n \circ d) \mid n>0 \rbrace]

Exercises 2 : Non-Recognizable Languages and Commutative closure

EX 1 : an abstract language

Lecture 3: Monadic Second Order Logic

digraph { rankdir=TB; NFTA -> EMSO -> MSO; MSO -> WSkS, NFTA; WSkS -> NFTA; }

Exercises 3:

EX 1: Bottom-up transducers

Lecture 4: wSkS

wSkS

Exercises 3: wSkS

EX 1: The power of wSkS

Algèbre

Algèbre.

Younesse Kaddar

Catégories

Algebre

Algorithmique

Anglais

Architecture-systeme

Biochemical-programming

Calculabilite

Categories-lambda-calculi

Categories-work

Club-algo

Complexity

Computational-geometric-learning

Computational-neuroscience

Computer-vision

Concurrency

Conferences