Salut,
Dans quelque temps, je vais commencer les TIPE (notez que je suis en sup et pas en spé) et je cherche des idées de sujets/plans qui pourraient le faire.
J'ai déjà commencé les recherches et je me suis (très superficiellement) intéressé aux applications des monoïdes en théorie des langages et théorie des codes. C'est sûrement intéressant, mais je n'ai pas d'idée de problématique (et apparemment, c'est cool d'en avoir une).
On m'a aussi proposé de parler des antivirus, y a une bonne partie théorique sur les machines de Turing visiblement. Mais encore une fois, le problème de la problématique (tiens, c'est drôle) se pose.
Si vous pouviez m'éclairer un peu sur ces points là, et même me donner d'autres idées ce serait génial !
Merci,
Edit : faute de frappe sur Turing.
24 réponse(s)
Pages:
1
-
2
|
colbseton
|
# - le Jeu 26 janvier à 23:22:40 - Répondre - Source |
|
En fait l'idée ce serait, comme tu l'as proposé, de prouver un résultat vu en cours (ou pas) grâce à Coq. Ce que je me demande maintenant, c'est de savoir si oui ou non on doit parler et expliquer les concepts qui sont derrière Coq et les assistants de preuves en général : j'ai évoqué la correspondance Curry-Howard, mais je pense aussi au lambda-calcul, aux types dépendants, etc.
|
|
Poulet
|
# - le Mer 09 mai à 11:42:22 - Répondre - Source |
|
Alors, où en es-tu ?
|
|
Holf
|
# - le Mer 09 mai à 14:50:27 - Répondre - Source |
|
Citation de colbseton
En fait l'idée ce serait, comme tu l'as proposé, de prouver un résultat vu en cours (ou pas) grâce à Coq. Ce que je me demande maintenant, c'est de savoir si oui ou non on doit parler et expliquer les concepts qui sont derrière Coq et les assistants de preuves en général : j'ai évoqué la correspondance Curry-Howard, mais je pense aussi au lambda-calcul, aux types dépendants, etc.
Ça me fait penser que la promo 2008-2009 de l'ENS Lyon avait pour projet intégré de créer des bibliothèques Coq pour couvrir au maximum le programme de math de prépa. Ça s'appelle coqtail : http://sourceforge.net/projects/coqtail/,http://coqtail.sourceforge.net/. Peut-être que ça peut t'intéresser !
|
|
colbseton
|
# - le Jeu 10 mai à 16:21:53 - Répondre - Source |
|
Merci bien, mais maintenant j'ai changé de TIPE pour faire un truc que certains trouveront moches : les graphes et les flots (flot max) :}. 'Faut dire qu'aussi on perdait vraiment pas mal de temps avec tous les concepts et les notations qui sont dans le Coq Art, du coup on voyait mal où on allait et ça partait dans tous les sens.
|
Pages:
1
-
2
Répondre à "Idées de TIPE"
Vous devez être connecté pour poster.