[TYPES/announce] Research Grant Position for 1 Year at the University of Udine

[Ivan Scagnetto]

A research grant position for one year in the field of Computer Aided Formal Reasoning is available at the University of Udine (Dept. of Mathematics, Computer Science and Physics). The research program is about the development of the core of a proof assistant based on LFP [1-6], a logical framework allowing to make calls to external oracles (e.g., other logical frameworks, decision methods etc.), starting from an existing type checker written in OCaml.



APPLICATION DEADLINE 07/09/2018 23:59 - Europe/Brussels



Further details:



https://euraxess.ec.europa.eu/jobs/330711



Notice of competition:



http://web.uniud.it/ateneo/normativa/albo_ufficiale/660%20-%202018/20180660.2%20Notice%20-%20ARIC.pdf



References



[1] F. Honsell, L. Liquori, P. Maksimovic and I. Scagnetto. Plugging-in proof development environments using Locks in LF. In Mathematical Structures in Computer Science, 1-28, 2018. doi:10.1017/S0960129518000105 [2] F. Honsell, L. Liquori, P. Maksimovic and I. Scagnetto. LLFP: A Logical Framework for Modeling External Evidence, Side Conditions, and Proof Irrelevance using Monads. In lmcs:3771 - Logical Methods in Computer Science, July 6, 2017, Volume 13, Issue 3.

[3] F. Honsell, M. Lenisa, L. Liquori, P. Maksimovic and I. Scagnetto. An Open Logical Framework. Journal of Logic and Computation (2016) 26 (1): 293-335.

[4] F. Honsell, L. Liquori, P. Maksimovic and I. Scagnetto. Gluing together Proof Environments: Canonical extensions of LF Type Theories featuring Locks. In Proc. of LFMTP 2015 (Logical Frameworks and Meta-Languages: Theory and Practice, Affiliated with CADE-25), Berlin, Germany, 01/08/2015, pp. 3--17, http://dx.doi.org/10.4204/EPTCS.185.1, ISSN: 2075-2180, Open Publishing Association.

[5] F. Honsell, L. Liquori and I. Scagnetto. LaxF: Side Conditions and External Evidence as Monads. In Proc. of MFCS 2014 (39th International Symposium on Mathematical Foundations of Computer Science), Part I, Budapest, Hungary, 25-29/08/2014, Lecture Notes in Computer Science, Vol. 8634, pages 327-339, Springer, ISBN 978-3-662-44521-1.

[6] F. Honsell, M. Lenisa, L. Liquori, P. Maksimovic and I. Scagnetto. LFP - A Logical Framework with External Predicates. In Proc. of LFMTP 2012 (7th International Workshop on Logical Frameworks and Meta-languages:

Theory and Practice), Copenhagen, Denmark - September 9, 2012.





-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20180829/9f703048/attachment.html>