# Classical Higher-Order Processes

Abstract : Classical Processes (CP) is a calculus where the proof theory of classical linear logic types processes à la $\pi$-calculus, building on a Curry-Howard correspondence between session types and linear propositions. We contribute to this research line by extending CP with process mobility, inspired by the Higher-Order $\pi$-calculus. The key to our calculus is that sequents are asymmetric: one side types sessions as in CP and the other types process variables, which can be instantiated with process values. The controlled interaction between the two sides ensures that process variables can be used at will, but always respecting the linear usage of sessions expected by the environment.
Type de document :
Communication dans un congrès
Ahmed Bouajjani; Alexandra Silva. 37th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2017, Neuchâtel, Switzerland. Springer International Publishing, Lecture Notes in Computer Science, LNCS-10321, pp.171-178, 2017, Formal Techniques for Distributed Objects, Components, and Systems. 〈10.1007/978-3-319-60225-7_12〉
Domaine :

https://hal.inria.fr/hal-01658427
Contributeur : Hal Ifip <>
Soumis le : jeudi 7 décembre 2017 - 15:49:23
Dernière modification le : jeudi 7 décembre 2017 - 15:50:42

### Fichier

##### Accès restreint
Fichier visible le : 2020-01-01

Connectez-vous pour demander l'accès au fichier

### Citation

Fabrizio Montesi. Classical Higher-Order Processes. Ahmed Bouajjani; Alexandra Silva. 37th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2017, Neuchâtel, Switzerland. Springer International Publishing, Lecture Notes in Computer Science, LNCS-10321, pp.171-178, 2017, Formal Techniques for Distributed Objects, Components, and Systems. 〈10.1007/978-3-319-60225-7_12〉. 〈hal-01658427〉

### Métriques

Consultations de la notice